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.
Tactic library in the Bellerophon tactic language.
Tactic library in the Bellerophon tactic language.
edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary
Main tactic library consisting of: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 CalculusAll tactics are implemented in the Bellerophon tactic language, including its dependent tactics, which ultimately produce edu.cmu.cs.ls.keymaerax.core.Provable proof certificates by the Bellerophon interpreter. The Provables that tactics produce can be extracted, for example, with edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.proveBy().
KeYmaera X supports many different proof styles, including flexible combinations of the following styles:
2. Explicit proofs use tactics to describe a proof directly mentioning all or most proof steps.
3. Proof by search relies mainly on proof search with occasional additional guidance.
4. Proof by pointing points out facts and where to use them.
5. Proof by congruence is based on equivalence or equality or implicational rewriting within a context.
6. Proof by chase is based on chasing away operators at an indicated position.
The most explicit types of proofs can be constructed directly using the edu.cmu.cs.ls.keymaerax.core.Provable certificates in KeYmaera X's kernel without using any tactics. Also see edu.cmu.cs.ls.keymaerax.core.
import edu.cmu.cs.ls.keymaerax.core._ // explicit proof certificate construction of |- !!p() <-> p() val proof = (Provable.startProof( "!!p() <-> p()".asFormula) (EquivRight(SuccPos(0)), 0) // right branch (NotRight(SuccPos(0)), 1) (NotLeft(AntePos(1)), 1) (Close(AntePos(0),SuccPos(0)), 1) // left branch (NotLeft(AntePos(0)), 0) (NotRight(SuccPos(1)), 0) (Close(AntePos(0),SuccPos(0)), 0) )
Explicit proofs construct similarly explicit proof steps, just with explicit tactics from TactixLibrary: The only actual difference is the order of the branches, which is fixed to be from left to right in tactic branching. Tactics also use more elegant signed integers to refer to antecedent positions (negative) or succedent positions (positive).
import TactixLibrary._ // Explicit proof tactic for |- !!p() <-> p() val proof = TactixLibrary.proveBy("!!p() <-> p()".asFormula, equivR(1) & <( (notL(-1) & notR(2) & closeId) , (notR(1) & notL(-2) & closeId) ) )
Proof by search primarily relies on proof search procedures to conduct a proof. That gives very short proofs but, of course, they are not always entirely informative about how the proof worked. It is easiest to see in simple situations where propositional logic proof search will find a proof but works well in more general situations, too.
import TactixLibrary._ // Proof by search of |- (p() & q()) & r() <-> p() & (q() & r()) val proof = TactixLibrary.proveBy("(p() & q()) & r() <-> p() & (q() & r())".asFormula, prop )
Common tactics for proof by search include edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.prop(), edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.auto() and the like.
Proof by pointing emphasizes the facts to use and is implicit about the details on how to use them exactly. Proof by pointing works by pointing to a position in the sequent and using a given fact at that position. For example, for proving
⟨v:=2*v+1;⟩v!=0 <-> 2*v+1!=0
it is enough to point to the highlighted position
using the Ax.diamond axiom fact
![a;]!p(||) <-> ⟨a;⟩p(||)
at the highlighted position to reduce the proof to a proof of
![v:=2*v+1;]!(v!=0) <-> 2*v+1!=0
which is, in turn, easy to prove by pointing to the highlighted position using the Ax.assignbAxiom axiom
[x:=t();]p(x) <-> p(t())
at the highlighted position to reduce the proof to
!!(2*v+1!=0) <-> 2*v+1!=0
Finally, using double negation !!p() <-> p()
at the highlighted position yields the following
2*v+1!=0 <-> 2*v+1!=0
which easily proves by reflexivity p() <-> p()
.
Proof by pointing matches the highlighted position against the highlighted position in the fact and does what it takes to use that knowledge. There are multiple variations of proof by pointing in edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.useAt and edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.byUS, which are also imported into edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary. The above proof by pointing implements directly in KeYmaera X:
import TactixLibrary._ // Proof by pointing of |- <v:=2*v+1;>v!=0 <-> 2*v+1!=0 val proof = TactixLibrary.proveBy("<v:=2*v+1;>q(v) <-> q(2*v+1)".asFormula, // use Ax.diamond axiom backwards at the indicated position on // |- __<v:=2*v+1;>q(v)__ <-> q(2*v+1) useExpansionAt(Ax.diamond)(1, 0::Nil) & // use Ax.assignbAxiom axiom forward at the indicated position on // |- !__[v:=2*v+1;]!q(v)__ <-> q(2*v+1) useAt(Ax.assignbAxiom(1, 0::0::Nil) & // use double negation at the indicated position on // |- __!!q(2*v+1)__ <-> q(2*v+1) useAt(Ax.doubleNegation)(1, 0::Nil) & // close by (an instance of) reflexivity |- p() <-> p() // |- q(2*v+1) <-> q(2*v+1) byUS(Ax.equivReflexive) )
Another example is:
import TactixLibrary._ // Proof by pointing of |- <a;++b;>p(x) <-> (<a;>p(x) | <b;>p(x)) val proof = TactixLibrary.proveBy("<a;++b;>p(x) <-> (<a;>p(x) | <b;>p(x))".asFormula, // use Ax.diamond axiom backwards at the indicated position on // |- __<a;++b;>p(x)__ <-> <a;>p(x) | <b;>p(x) useExpansionAt(Ax.diamond)(1, 0::Nil) & // use Ax.choiceb axiom forward at the indicated position on // |- !__[a;++b;]!p(x)__ <-> <a;>p(x) | <b;>p(x) useAt(Ax.choiceb)(1, 0::0::Nil) & // use Ax.diamond axiom forward at the indicated position on // |- !([a;]!p(x) & [b;]!p(x)) <-> __<a;>p(x)__ | <b;>p(x) useExpansionAt(Ax.diamond)(1, 1::0::Nil) & // use Ax.diamond axiom forward at the indicated position on // |- !([a;]!p(x) & [b;]!p(x)) <-> ![a;]!p(x) | __<b;>p(x)__ useExpansionAt(Ax.diamond)(1, 1::1::Nil) & // use propositional logic to show // |- !([a;]!p(x) & [b;]!p(x)) <-> ![a;]!p(x) | ![b;]!p(x) prop )
edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.stepAt also uses proof by pointing but figures out the appropriate fact to use on its own. Here's a similar proof:
import TactixLibrary._ // Proof by pointing with steps of |- ⟨a++b⟩p(x) <-> (⟨a⟩p(x) | ⟨b⟩p(x)) val proof = TactixLibrary.proveBy("p(x) <-> (p(x) | p(x))".asFormula, // use Ax.diamond axiom backwards at the indicated position on // |- __⟨a++b⟩p(x)__ <-> ⟨a⟩p(x) | ⟨b⟩p(x) useExpansionAt(Ax.diamond)(1, 0::Nil) & // |- !__[a;++b;]!p(x)__ <-> ⟨a⟩p(x) | ⟨b⟩p(x) // step Ax.choiceb axiom forward at the indicated position stepAt(1, 0::0::Nil) & // |- __!([a;]!p(x) & [b;]!p(x))__ <-> ⟨a⟩p(x) | ⟨b⟩p(x) // step deMorgan forward at the indicated position stepAt(1, 0::Nil) & // |- __![a;]!p(x)__ | ![b;]!p(x) <-> ⟨a⟩p(x) | ⟨b⟩p(x) // step Ax.diamond forward at the indicated position stepAt(1, 0::0::Nil) & // |- ⟨a⟩p(x) | __![b;]!p(x)__ <-> ⟨a⟩p(x) | ⟨b⟩p(x) // step Ax.diamond forward at the indicated position stepAt(1, 0::1::Nil) & // |- ⟨a⟩p(x) | ⟨b⟩p(x) <-> ⟨a⟩p(x) | ⟨b⟩p(x) byUS(Ax.equivReflexive) )
Likewise, for proving
x>5 |- !([x:=x+1; ++ x:=0;]x>=6) | x<2
it is enough to point to the highlighted position
x>5 |- !([x:=x+1; ++ x:=0;]x>=6) | x<2
and using the Ax.choiceb axiom fact
[a;++b;]p(||) <-> [a;]p(||) & [b;]p(||)
to reduce the proof to a proof of
x>5 |- !([x:=x+1;]x>6 & [x:=0;]x>=6) | x<2
which is, in turn, easy to prove by pointing to the assignments using Ax.assignbAxiom axioms and ultimately asking propositional logic.
More proofs by pointing are shown in edu.cmu.cs.ls.keymaerax.btactics.Ax source code.
Proof by congruence is based on equivalence or equality or implicational rewriting within a context. This proof style can make quite quick inferences leading to significant progress using the CE, CQ, CT congruence proof rules or combinations thereof.
import TactixLibrary._ // |- x*(x+1)>=0 -> [y:=0;x:=__x^2+x__;]x>=y val proof = TactixLibrary.proveBy("x*(x+1)>=0 -> [y:=0;x:=x^2+x;]x>=y".asFormula, CEat(proveBy("x*(x+1)=x^2+x".asFormula, QE)) (1, 1::0::1::1::Nil) & // |- x*(x+1)>=0 -> [y:=0;x:=__x*(x+1)__;]x>=y by CE/CQ using x*(x+1)=x^2+x at the indicated position // step uses top-level operator [;] stepAt(1, 1::Nil) & // |- x*(x+1)>=0 -> [y:=0;][x:=x*(x+1);]x>=y // step uses top-level operator [:=] stepAt(1, 1::Nil) & // |- x*(x+1)>=0 -> [x:=x*(x+1);]x>=0 // step uses top-level [:=] stepAt(1, 1::Nil) & // |- x*(x+1)>=0 -> x*(x+1)>=0 prop )
Proof by congruence can also make use of a fact in multiple places at once by defining an appropriate context C:
import TactixLibrary._ val C = Context("x<5 & ⎵ -> [{x' = 5*x & ⎵}](⎵ & x>=1)".asFormula) // |- x<5 & __x^2<4__ -> [{x' = 5*x & __x^2<4__}](__x^2<4__ & x>=1) val proof = TactixLibrary.proveBy("x<5 & x^2<4 -> [{x' = 5*x & x^2<4}](x^2<4 & x>=1)".asFormula, CEat(proveBy("-2x^2<4" .asFormula, QE), C) (1)) ) // |- x<5 & (__-2[{x' = 5*x & __-2 println(proof.subgoals)=1) by CE
Proof by chase chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices. The canonical examples use edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chase() to chase away differential forms:
import TactixLibrary._ val proof = TactixLibrary.proveBy("[{x'=22}](2*x+x*y>=5)'".asFormula, // chase the differential prime away in the postcondition chase(1, 1 :: Nil) // |- [{x'=22}]2*x'+(x'*y+x*y')>=0 ) // Remaining subgoals: |- [{x'=22}]2*x'+(x'*y+x*y')>=0 println(proof.subgoals)
import TactixLibrary._ val proof = TactixLibrary.proveBy("[{x'=22}](2*x+x*y>=5)' <-> [{x'=22}]2*x'+(x'*y+x*y')>=0".asFormula, // chase the differential prime away in the left postcondition chase(1, 0:: 1 :: Nil) & // |- [{x'=22}]2*x'+(x'*y+x*y')>=0 <-> [{x'=22}]2*x'+(x'*y+x*y')>=0 byUS(Ax.equivReflexive) )
Yet edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chase() is also useful to chase away other operators, say, modalities:
import TactixLibrary._ // proof by chase of |- [?x>0;x:=x+1;x:=2*x; ++ ?x=0;x:=1;]x>=1 val proof = TactixLibrary.proveBy( "[?x>0;x:=x+1;x:=2*x; ++ ?x=0;x:=1;]x>=1".asFormula, // chase the box in the succedent away chase(1,Nil) & // |- (x>0->2*(x+1)>=1)&(x=0->1>=1) QE )
Provable=>Provable
Provable=>Provable
Position=>(Provable=>Provable)
Expand descriptions
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
edu.cmu.cs.ls.keymaerax.btactics.DifferentialEquationCalculus
Helper functions for implementing tactics.
Helper functions for implementing tactics. Note that these are **not** themselves tactics.
helpers.DifferentialHelper Differential Equation-specific program helpers.
helpers.ProgramHelpers Hybrid Program helpers that are not specific to Differential Equations.
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
,Program
Sequent
- Sequents of formulasProvable
- Proof certificates transformed by rules/axiomsRule
- Proof rules as well asUSubstOne
for (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.kyx
filesDLParser
- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser
- Combinator parser reading KeYmaera X model and proof archive.kyx
filesedu.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-help
to 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