rootdoc.txt

=KeYmaera X: An aXiomatic Tactical Theorem Prover=

[[http://keymaeraX.org/ KeYmaera X]] is a theorem prover for [[https://lfcps.org/logic/dL.html 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/]]

  [[http://keymaeraX.org/doc/dL-grammar.md Concrete syntax for input language Differential Dynamic Logic]]

==Package Structure==

Main documentation entry points for KeYmaera X API:

  - `[[org.keymaerax.core]]` - KeYmaera X kernel, proof certificates, main data structures
      - `[[org.keymaerax.core.Expression Expression]]` - Differential dynamic logic expressions:
        `[[org.keymaerax.core.Term Term]]`,
        `[[org.keymaerax.core.Formula Formula]]`,
        `[[org.keymaerax.core.Program Program]]`
      - `[[org.keymaerax.core.Sequent Sequent]]` - Sequents of formulas
      - `[[org.keymaerax.core.Provable Provable]]` - Proof certificates transformed by rules/axioms
      - `[[org.keymaerax.core.Rule Rule]]` - Proof rules as well as `[[org.keymaerax.core.USubstOne USubstOne]]` for (one-pass) uniform substitutions and [[org.keymaerax.core.URename renaming]].
      - `[[org.keymaerax.core.StaticSemantics StaticSemantics]]` - Static semantics with free and bound variable analysis
      - Instead of constructing dL expressions from constructors, it is easier to use the `[[org.keymaerax.parser.KeYmaeraXParser KeYmaeraXParser]]`.

  - `[[org.keymaerax.parser]]` - Parser and pretty printer with concrete syntax and notation for differential dynamic logic.

      - [[http://keymaeraX.org/doc/dL-grammar.md Concrete syntax for input language Differential Dynamic Logic]]
      - `[[org.keymaerax.parser.KeYmaeraXPrettyPrinter KeYmaeraXPrettyPrinter]]` - Pretty printer producing concrete KeYmaera X syntax
      - `[[org.keymaerax.parser.KeYmaeraXParser KeYmaeraXParser]]` - Parser reading concrete KeYmaera X syntax
      - `[[org.keymaerax.parser.DLParser DLParser]]` - Combinator parser reading concrete KeYmaera X syntax
      - `[[org.keymaerax.parser.DLArchiveParser DLArchiveParser]]` - Combinator parser reading KeYmaera X model and proof archive `.kyx` files

  - `[[org.keymaerax.infrastruct]]` - Prover infrastructure outside the kernel
      - `[[org.keymaerax.infrastruct.UnificationMatch UnificationMatch]]` - Unification algorithm
      - `[[org.keymaerax.infrastruct.RenUSubst RenUSubst]]` - Renaming Uniform Substitution quickly combining kernel's renaming and substitution.
      - `[[org.keymaerax.infrastruct.Context Context]]` - Representation for contexts of formulas in which they occur.
      - `[[org.keymaerax.infrastruct.Augmentors Augmentors]]` - Augmenting formula and expression data structures with additional functionality
      - `[[org.keymaerax.infrastruct.ExpressionTraversal ExpressionTraversal]]` - Generic traversal functionality for expressions

  - `[[org.keymaerax.bellerophon]]` - Bellerophon tactic language and tactic interpreter
      - `[[org.keymaerax.bellerophon.BelleExpr BelleExpr]]` - Tactic language expressions
      - `[[org.keymaerax.bellerophon.SequentialInterpreter SequentialInterpreter]]` - Sequential tactic interpreter for Bellerophon tactics

  - `[[org.keymaerax.btactics]]` - Bellerophon tactic library for conducting proofs.
      - `[[org.keymaerax.btactics.TactixLibrary TactixLibrary]]` - Main KeYmaera X tactic library including many proof tactics.
      - `[[org.keymaerax.btactics.HilbertCalculus HilbertCalculus]]` - Hilbert Calculus for differential dynamic logic
      - `[[org.keymaerax.btactics.SequentCalculus SequentCalculus]]` - Sequent Calculus for propositional and first-order logic
      - `[[org.keymaerax.btactics.HybridProgramCalculus HybridProgramCalculus]]` - Hybrid Program Calculus for differential dynamic logic
      - `[[org.keymaerax.btactics.DifferentialEquationCalculus DifferentialEquationCalculus]]` - Differential Equation Calculus for differential dynamic logic
      - `[[org.keymaerax.btactics.UnifyUSCalculus UnifyUSCalculus]]` - Unification-based uniform substitution calculus underlying the other calculi
      - `[org.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic]` - Forward tactic framework for conducting proofs from premises to conclusions

  - `[[org.keymaerax.lemma]]` - Lemma mechanism
      - `[[org.keymaerax.lemma.Lemma Lemma]]` - Lemmas are [[org.keymaerax.core.Provable Provables]] stored under a name, e.g., in files.
      - `[[org.keymaerax.lemma.LemmaDB LemmaDB]]` - Lemma database stored in files or database etc.

  - `[[org.keymaerax.tools.qe]]` - Real arithmetic back-end solvers
      - `[[org.keymaerax.tools.qe.MathematicaQETool MathematicaQETool]]` - Mathematica interface for real arithmetic.
      - `[[org.keymaerax.tools.qe.Z3QETool Z3QETool]]` - Z3 interface for real arithmetic.
  - `[[org.keymaerax.tools.ext]]` - Extended back-ends for noncritical ODE solving, counterexamples, algebra, simplifiers, etc.
      - `[[org.keymaerax.tools.ext.Mathematica  Mathematica]]` - Mathematica interface for ODE solving, algebra, simplification, invariant generation, etc.
      - `[[org.keymaerax.tools.ext.Z3 Z3]]` - Z3 interface for real arithmetic including simplifiers.
    
==Entry Points==

Additional entry points and usage points for KeYmaera X API:

  - `[[org.keymaerax.launcher.KeYmaeraX]]` - Command-line launcher for KeYmaera X supports command-line argument `-help` to obtain usage information

  - `[[org.keymaerax.btactics.AxIndex]]` - Axiom indexing data structures with keys and recursors for canonical proof strategies.

  - `[[org.keymaerax.btactics.macros.Axiom]` `[[org.keymaerax.btactics.DerivationInfo]]` - Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.

  - `[[org.keymaerax.bellerophon.UIIndex]]` - Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.

  - `[[org.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. 
[[https://doi.org/10.1007/s10817-016-9385-1 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. 
[[https://doi.org/10.1007/978-3-319-21401-6_36 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.
[[https://doi.org/10.1007/978-3-319-63588-0 Logical Foundations of Cyber-Physical Systems]].
Springer, 2018.
[[http://video.lfcps.org/ Videos]]