# root package
**

#### package root

### 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.

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- Instead of constructing dL expressions from constructors, it is easier to use the
`KeYmaeraXParser`

.

`edu.cmu.cs.ls.keymaerax.parser`

- Parser and pretty printer with concrete syntax and notation for differential dynamic logic.- Concrete syntax for input language 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`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

**

**

- Alphabetic

- Public
- All

## 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