Packages

package root

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.

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

Definition Classes: root

package edu

Definition Classes: root

package cmu

Definition Classes: edu

package cs

Definition Classes: cmu

package ls

Definition Classes: cs

package keymaerax

Definition Classes: ls

package launcher

KeYmaera X command line launcher for starting its main program with the web UI.

Definition Classes: keymaerax
To do: Stub. Describe for real.

CLILoadingDialog

CoasterXMain

GraphicalLoadingDialog

KeYmaeraX

LoadingDialog

LoadingDialogFactory

Main

SystemWebBrowser

edu.cmu.cs.ls.keymaerax.launcher

KeYmaeraX

object KeYmaeraX

Command-line interface launcher for KeYmaera X, the aXiomatic Tactical Theorem Prover for Hybrid Systems and Hybrid Games.

- edu.cmu.cs.ls.keymaerax.core - KeYmaera X kernel, proof certificates, main data structures - edu.cmu.cs.ls.keymaerax.btactics - Tactic language library - edu.cmu.cs.ls.keymaerax.bellerophon - Bellerophon tactic language and tactic interpreter

See also: Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. arXiv 1503.01981
Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.
Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Volp and Andre 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, LNCS. Springer, 2015.
Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980
Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. IEEE 2012
edu.cmu.cs.ls.keymaerax.launcher.Main

Linear Supertypes

AnyRef, Any

Ordering

Alphabetic
By Inheritance

Inherited

KeYmaeraX
AnyRef
Any

Hide All
Show All

Visibility

Public
All

Type Members

class KeYmaeraXSecurityManager extends SecurityManager
Implements the security policy for the KeYmaera X web server.
Implements the security policy for the KeYmaera X web server.
Preferably we would heavily restrict uses of reflection (to prevent, for example, creating fake Provables), but we know of no way to do so except relying on extremely fragile methods such as crawling the call stack. The same goes for restricting read access to files.
Instead we settle for preventing people from installing less-restrictive security managers and restricting all writes to be inside the .keymaerax directory.

Value Members

final def !=(arg0: Any): Boolean

Definition Classes
AnyRef → Any
final def ##(): Int

Definition Classes
AnyRef → Any
final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
var LAUNCH: Boolean
final def asInstanceOf[T0]: T0

Definition Classes
Any
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@native() @throws( ... )
def convertTactics(options: OptionMap, usage: String): Unit
Executes all entries in options('in) to convert their tactics into options('conversion) format.
Executes all entries in options('in) to convert their tactics into options('conversion) format. Prints the result to options('out).
final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@native()
def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@native()
def help: String
KeYmaera X -help string.
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
def launchUI(args: Array[String]): Unit
Launch the web user interface
def main(args: Array[String]): Unit
main function to start KeYmaera X from command line.
main function to start KeYmaera X from command line. Other entry points exist but this one is best for command line interfaces.
def modelplex(options: OptionMap): Unit
ModelPlex monitor synthesis for the given input files
ModelPlex monitor synthesis for the given input files
```
KeYmaeraXPrettyPrinter(ModelPlex(vars)(KeYmaeraXProblemParser(input))
```
options
in describes input file name, vars describes the list of variables, out describes the output file name.
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
def nextOption(map: OptionMap, list: List[String]): OptionMap

Annotations
@tailrec()
final def notify(): Unit

Definition Classes
AnyRef
Annotations
@native()
final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@native()
def printNode(node: Sequent): Unit
def printOpenGoals(node: ProvableSig): Unit
Print brief information about all open goals in the proof tree under node
def repl(options: OptionMap): Unit
def stats: String
Statistics about size of prover kernel.
final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
def toString(): String

Definition Classes
AnyRef → Any
val usage: String
Usage -help information.
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@native() @throws( ... )
object Modes
Names of actions that full KeYmaera X supports.

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

KeYmaeraX

object KeYmaeraX

Type Members

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

KeYmaeraX 

object KeYmaeraX

Type Members

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

KeYmaeraX