rootdoc.txt

==KeYmaera X: An aXiomatic Tactical Theorem Prover==
====================================================

[[http://keymaeraX.org/ KeYmaera X]] is a theorem prover for [[http://www.cs.cmu.edu/~aplatzer/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:

  - `[[edu.cmu.cs.ls.keymaerax.core]]` - KeYmaera X kernel, proof certificates, main data structures
      - `[[edu.cmu.cs.ls.keymaerax.core.Expression]]` - Differential dynamic logic expressions
      - `[[edu.cmu.cs.ls.keymaerax.core.Sequent]]` - Sequents of formulas
      - `[[edu.cmu.cs.ls.keymaerax.core.Rule]]` - Proof rules
      - `[[edu.cmu.cs.ls.keymaerax.core.Provable]]` - Proof certificate

  - `[[edu.cmu.cs.ls.keymaerax.btactics]]` - Tactic language library
      - `[[edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary]]` - Main tactic library
      - `[[edu.cmu.cs.ls.keymaerax.btactics.HilbertCalculus]]` - Hilbert Calculus for differential dynamic logic
      - `[[edu.cmu.cs.ls.keymaerax.btactics.SequentCalculus]]` - Sequent Calculus for propositional and first-order logic
      - `[[edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus]]` - Unification-based Uniform Substitution Calculus

  - `[[edu.cmu.cs.ls.keymaerax.bellerophon]]` - Bellerophon tactic language and tactic interpreter
      - `[[edu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr]]` - Tactic language expressions
      - `[[edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter]]` - Sequential tactic interpreter

  - `[[edu.cmu.cs.ls.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]]
      - `[[edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser]]` - Parser for concrete KeYmaera X syntax
      - `[[edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter]]` - Pretty printer for concrete KeYmaera X syntax
      - `[[edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXProblemParser]]` - Parser for KeYmaera X problem files `.kyx`

  - `[[edu.cmu.cs.ls.keymaerax.lemma]]` - Lemma mechanism
      - `[[edu.cmu.cs.ls.keymaerax.lemma.FileLemmaDB]]` - Lemma database stored in files

  - `[[edu.cmu.cs.ls.keymaerax.tools]]` - Arithmetic back-ends
      - `[[edu.cmu.cs.ls.keymaerax.tools.Mathematica]]` - Mathematica interface for real arithmetic and ODE solver etc.
      - `[[edu.cmu.cs.ls.keymaerax.tools.Z3]]` - Z3 interface for real arithmetic.
      - `[[edu.cmu.cs.ls.keymaerax.tools.Polya]]` - Polya interface for real arithmetic.
    
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.DerivationInfo]]` - Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.

==References==

Full references are provided elsewhere [[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, LNCS. Springer, 2015. 

3. André Platzer.
[[https://doi.org/10.1007/978-3-319-63588-0 Logical Foundations of Cyber-Physical Systems]].
Springer, 2018.