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.

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.

UnifyUSCalculus - 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 conclusions

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.

## 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 structures`Expression`

- Differential dynamic logic expressions:`Term`

,`Formula`

,`Program`

`Sequent`

- Sequents of formulas`Provable`

- Proof certificates transformed by rules/axioms`Rule`

- Proof rules as well as`USubstOne`

for (one-pass) uniform substitutions and renaming.`StaticSemantics`

- Static semantics with free and bound variable analysis`KeYmaeraXParser`

.`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 syntax`KeYmaeraXParser`

- Parser reading concrete KeYmaera X syntax`KeYmaeraXArchiveParser`

- Parser reading KeYmaera X model and proof archive`.kyx`

files`DLParser`

- Combinator parser reading concrete KeYmaera X syntax`DLArchiveParser`

- Combinator parser reading KeYmaera X model and proof archive`.kyx`

files`edu.cmu.cs.ls.keymaerax.infrastruct`

- Prover infrastructure outside the kernel`UnificationMatch`

- Unification algorithm`RenUSubst`

- 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 functionality`ExpressionTraversal`

- Generic traversal functionality for expressions`edu.cmu.cs.ls.keymaerax.bellerophon`

- Bellerophon tactic language and tactic interpreter`BelleExpr`

- Tactic language expressions`SequentialInterpreter`

- Sequential tactic interpreter for Bellerophon tactics`edu.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 logic`SequentCalculus`

- Sequent Calculus for propositional and first-order logic`HybridProgramCalculus`

- Hybrid Program Calculus for differential dynamic logic`DifferentialEquationCalculus`

- Differential Equation Calculus for differential dynamic logic`UnifyUSCalculus`

- 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 conclusions`edu.cmu.cs.ls.keymaerax.lemma`

- Lemma mechanism`Lemma`

- 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 solvers`MathematicaQETool`

- 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 information`edu.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