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 pretty-printed 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 143-189, 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(pos:edu\.cmu\.cs\.ls\.keymaerax\.core\.SeqPos):edu\.cmu\.cs\.ls\.keymaerax\.core\.Formula*
-
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(pos:edu\.cmu\.cs\.ls\.keymaerax\.core\.SeqPos):edu\.cmu\.cs\.ls\.keymaerax\.core\.Formula*
-
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
Pretty-print 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
A copy of this sequent with the indicated succedent position replaced by gluing the sequent s, same as updated(p:edu\.cmu\.cs\.ls\.keymaerax\.core\.SeqPos,s:edu\.cmu\.cs\.ls\.keymaerax\.core\.Sequent):edu\.cmu\.cs\.ls\.keymaerax\.core\.Sequent*
-
def
updated(p: AntePos, s: Sequent): Sequent
A copy of this sequent with the indicated antecedent position replaced by gluing the sequent s, same as updated(p:edu\.cmu\.cs\.ls\.keymaerax\.core\.SeqPos,s:edu\.cmu\.cs\.ls\.keymaerax\.core\.Sequent):edu\.cmu\.cs\.ls\.keymaerax\.core\.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.
-
def
updated(p: SuccPos, f: Formula): Sequent
A copy of this sequent with the indicated succedent position replaced by the formula f, same as Sequent.updated(p:edu\.cmu\.cs\.ls\.keymaerax\.core\.SeqPos,f:edu\.cmu\.cs\.ls\.keymaerax\.core\.Formula):edu\.cmu\.cs\.ls\.keymaerax\.core\.Sequent*.
-
def
updated(p: AntePos, f: Formula): Sequent
A copy of this sequent with the indicated antecedent position replaced by the formula f, same as Sequent.updated(p:edu\.cmu\.cs\.ls\.keymaerax\.core\.SeqPos,f:edu\.cmu\.cs\.ls\.keymaerax\.core\.Formula):edu\.cmu\.cs\.ls\.keymaerax\.core\.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 structuresExpression- Differential dynamic logic expressions:Term,Formula,ProgramSequent- Sequents of formulasProvable- Proof certificates transformed by rules/axiomsRule- Proof rules as well asUSubstOnefor (one-pass) uniform substitutions and renaming.StaticSemantics- Static semantics with free and bound variable analysisKeYmaeraXParser.edu.cmu.cs.ls.keymaerax.parser- Parser and pretty printer with concrete syntax and notation for differential dynamic logic.KeYmaeraXPrettyPrinter- Pretty printer producing concrete KeYmaera X syntaxKeYmaeraXParser- Parser reading concrete KeYmaera X syntaxKeYmaeraXArchiveParser- Parser reading KeYmaera X model and proof archive.kyxfilesDLParser- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser- Combinator parser reading KeYmaera X model and proof archive.kyxfilesedu.cmu.cs.ls.keymaerax.infrastruct- Prover infrastructure outside the kernelUnificationMatch- Unification algorithmRenUSubst- Renaming Uniform Substitution quickly combining kernel's renaming and substitution.Context- Representation for contexts of formulas in which they occur.Augmentors- Augmenting formula and expression data structures with additional functionalityExpressionTraversal- Generic traversal functionality for expressionsedu.cmu.cs.ls.keymaerax.bellerophon- Bellerophon tactic language and tactic interpreterBelleExpr- Tactic language expressionsSequentialInterpreter- Sequential tactic interpreter for Bellerophon tacticsedu.cmu.cs.ls.keymaerax.btactics- Bellerophon tactic library for conducting proofs.TactixLibrary- Main KeYmaera X tactic library including many proof tactics.HilbertCalculus- Hilbert Calculus for differential dynamic logicSequentCalculus- Sequent Calculus for propositional and first-order logicHybridProgramCalculus- Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus- Differential Equation Calculus for differential dynamic logicUnifyUSCalculus- Unification-based uniform substitution calculus underlying the other calculi[edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic]- Forward tactic framework for conducting proofs from premises to conclusionsedu.cmu.cs.ls.keymaerax.lemma- Lemma mechanismLemma- Lemmas are Provables stored under a name, e.g., in files.LemmaDB- Lemma database stored in files or database etc.edu.cmu.cs.ls.keymaerax.tools.qe- Real arithmetic back-end solversMathematicaQETool- Mathematica interface for real arithmetic.Z3QETool- Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext- Extended back-ends for noncritical ODE solving, counterexamples, algebra, simplifiers, etc.Mathematica- Mathematica interface for ODE solving, algebra, simplification, invariant generation, etc.Z3- Z3 interface for real arithmetic including simplifiers.Entry Points
Additional entry points and usage points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX- Command-line launcher for KeYmaera X supports command-line argument-helpto obtain usage informationedu.cmu.cs.ls.keymaerax.btactics.AxIndex- Axiom indexing data structures with keys and recursors for canonical proof strategies.edu.cmu.cs.ls.keymaerax.btactics.DerivationInfo- Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.edu.cmu.cs.ls.keymaerax.bellerophon.UIIndex- Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.edu.cmu.cs.ls.keymaerax.btactics.Ax- Registry for derived axioms and axiomatic proof rules that are proved from the core.References
Full references on KeYmaera X are provided at 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. 219-265, 2017.
2. Nathan Fulton, Stefan Mitsch, Jan-David 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, volume 9195 of LNCS, pp. 527-538. Springer, 2015.
3. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. Videos