final case class Sequent(ante: IndexedSeq[Formula], succ: IndexedSeq[Formula]) extends Product with Serializable
Sequent ante  succ
with antecedent ante and succedent succ.
ante(0),ante(1),...,ante(n)  succ(0),succ(1),...,succ(m)
This sequent is often prettyprinted with signed line numbers:
1: ante(0) 2: ante(1) ... (n+1): ante(n) ==> 1: succ(0) 2: succ(1) ... (m+1): succ(m)
The semantics of sequent ante  succ
is the conjunction of the formulas in ante
implying
the disjunction of the formulas in succ
.
 ante
The ordered list of antecedents of this sequent whose conjunction is assumed.
 succ
The orderd list of succedents of this sequent whose disjunction needs to be shown.
 See also
Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143189, 2008.
 Alphabetic
 By Inheritance
 Sequent
 Serializable
 Serializable
 Product
 Equals
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Instance Constructors
Value Members

final
def
!=(arg0: Any): Boolean
 Definition Classes
 AnyRef → Any

final
def
##(): Int
 Definition Classes
 AnyRef → Any

final
def
==(arg0: Any): Boolean
 Definition Classes
 AnyRef → Any
 val ante: IndexedSeq[Formula]

def
apply(pos: SuccPos): Formula
Retrieves the formula in sequent at a given antecedent position.
Retrieves the formula in sequent at a given antecedent position.
 pos
the antecedent position of the formula
 returns
the formula at the given position from the antecedent
 Note
slightly faster version with the same result as Sequent.apply(SeqPos)

def
apply(pos: AntePos): Formula
Retrieves the formula in sequent at a given succedent position.
Retrieves the formula in sequent at a given succedent position.
 pos
the succedent position of the formula
 returns
the formula at the given position from the succedent
 Note
slightly faster version with the same result as Sequent.apply(SeqPos)

def
apply(pos: SeqPos): Formula
Retrieves the formula in sequent at a given position.
Retrieves the formula in sequent at a given position.
 pos
the position of the formula
 returns
the formula at the given position either from the antecedent or the succedent

final
def
asInstanceOf[T0]: T0
 Definition Classes
 Any

def
clone(): AnyRef
 Attributes
 protected[java.lang]
 Definition Classes
 AnyRef
 Annotations
 @native() @throws( ... )

final
def
eq(arg0: AnyRef): Boolean
 Definition Classes
 AnyRef

def
finalize(): scala.Unit
 Attributes
 protected[java.lang]
 Definition Classes
 AnyRef
 Annotations
 @throws( classOf[java.lang.Throwable] )

final
def
getClass(): Class[_]
 Definition Classes
 AnyRef → Any
 Annotations
 @native()

def
glue(s: Sequent): Sequent
A copy of this sequent concatenated with given sequent s.
A copy of this sequent concatenated with given sequent s. Sequent(A,S) glue Sequent(B,T) == Sequent(A++B, S++T)
 s
the sequent whose antecedent to append to ours and whose succedent to append to ours.
 returns
a copy of this sequent concatenated with s. Results in a least upper bound with respect to subsets of this and s.

final
def
isInstanceOf[T0]: Boolean
 Definition Classes
 Any

final
def
ne(arg0: AnyRef): Boolean
 Definition Classes
 AnyRef

final
def
notify(): scala.Unit
 Definition Classes
 AnyRef
 Annotations
 @native()

final
def
notifyAll(): scala.Unit
 Definition Classes
 AnyRef
 Annotations
 @native()

def
prettyString: String
Prettyprint sequent

def
sameSequentAs(r: Sequent): Boolean
Check whether this sequent is the same as the given sequent r (considered as sets)
Check whether this sequent is the same as the given sequent r (considered as sets)
 Note
Used for contracts in the core.

def
subsequentOf(r: Sequent): Boolean
Check whether this sequent is a subsequent of the given sequent r (considered as sets)
Check whether this sequent is a subsequent of the given sequent r (considered as sets)
 Note
Used for contracts in the core.
 val succ: IndexedSeq[Formula]

final
def
synchronized[T0](arg0: ⇒ T0): T0
 Definition Classes
 AnyRef

def
toString(): String
 Definition Classes
 Sequent → AnyRef → Any
 def updated(p: SuccPos, s: Sequent): Sequent
 def updated(p: AntePos, s: Sequent): Sequent

def
updated(p: SeqPos, s: Sequent): Sequent
A copy of this sequent with the indicated position replaced by gluing the sequent s.
A copy of this sequent with the indicated position replaced by gluing the sequent s.
 p
the position of the replacement
 s
the sequent glued / concatenated to this sequent after dropping p.
 returns
a copy of this sequent with the formula at position p removed and the sequent s appended.
 See also
Sequent.glue(Sequent)
Sequent.updated(Position,Formula)
 def updated(p: SuccPos, f: Formula): Sequent
 def updated(p: AntePos, f: Formula): Sequent

def
updated(p: SeqPos, f: Formula): Sequent
A copy of this sequent with the indicated position replaced by the formula f.
A copy of this sequent with the indicated position replaced by the formula f.
 p
the position of the replacement
 f
the replacing formula
 returns
a copy of this sequent with the formula at position p replaced by f.

final
def
wait(): scala.Unit
 Definition Classes
 AnyRef
 Annotations
 @throws( ... )

final
def
wait(arg0: Long, arg1: Int): scala.Unit
 Definition Classes
 AnyRef
 Annotations
 @throws( ... )

final
def
wait(arg0: Long): scala.Unit
 Definition Classes
 AnyRef
 Annotations
 @native() @throws( ... )
KeYmaera X: An aXiomatic Tactical Theorem Prover
KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics. Reasoning about complicated hybrid systems requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute tactics in parallel, and interface with partial proofs via an extensible user interface.
http://keymaeraX.org/
Concrete syntax for input language Differential Dynamic Logic
Package Structure
Main documentation entry points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.core
 KeYmaera X kernel, proof certificates, main data structuresedu.cmu.cs.ls.keymaerax.core.Expression
 Differential dynamic logic expressionsedu.cmu.cs.ls.keymaerax.core.Sequent
 Sequents of formulasedu.cmu.cs.ls.keymaerax.core.Rule
 Proof rulesedu.cmu.cs.ls.keymaerax.core.Provable
 Proof certificateedu.cmu.cs.ls.keymaerax.btactics
 Tactic language libraryedu.cmu.cs.ls.keymaerax.btactics.TactixLibrary
 Main tactic libraryedu.cmu.cs.ls.keymaerax.btactics.HilbertCalculus
 Hilbert Calculus for differential dynamic logicedu.cmu.cs.ls.keymaerax.btactics.SequentCalculus
 Sequent Calculus for propositional and firstorder logicedu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus
 Unificationbased Uniform Substitution Calculusedu.cmu.cs.ls.keymaerax.bellerophon
 Bellerophon tactic language and tactic interpreteredu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr
 Tactic language expressionsedu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter
 Sequential tactic interpreteredu.cmu.cs.ls.keymaerax.parser
 Parser and pretty printer with concrete syntax and notation for differential dynamic logic.edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser
 Parser for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter
 Pretty printer for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXProblemParser
 Parser for KeYmaera X problem files.kyx
edu.cmu.cs.ls.keymaerax.lemma
 Lemma mechanismedu.cmu.cs.ls.keymaerax.lemma.FileLemmaDB
 Lemma database stored in filesedu.cmu.cs.ls.keymaerax.tools
 Arithmetic backendsedu.cmu.cs.ls.keymaerax.tools.Mathematica
 Mathematica interface for real arithmetic and ODE solver etc.edu.cmu.cs.ls.keymaerax.tools.Z3
 Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.Polya
 Polya interface for real arithmetic.Additional entry points and usage points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX
 Commandline launcher for KeYmaera X supports commandline argumenthelp
to obtain usage informationedu.cmu.cs.ls.keymaerax.btactics.DerivationInfo
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface info.References
Full references are provided elsewhere http://keymaeraX.org/, the main references are the following:
1. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219265, 2017.
2. Nathan Fulton, Stefan Mitsch, JanDavid Quesel, Marcus Völp and André Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.