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 tools

Arithmetic back-ends and arithmetic utilities for tactics, including an SMT interface.

edu.cmu.cs.ls.keymaerax.tools.ext.Mathematica - Mathematica interface for real arithmetic and ODE solver etc.
edu.cmu.cs.ls.keymaerax.tools.ext.Z3 - Z3 interface for real arithmetic.
edu.cmu.cs.ls.keymaerax.tools.qe.SMTConverter - SMT converter for real arithmetic.

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

package qe

Definition Classes: tools

BaseMathematicaCommandRunner

BigDecimalQETool

BinaryMathOpSpec

DefaultSMTConverter

ExprFactory

InterpretedMathOpSpec

JLinkMathematicaCommandRunner

K2MConverter

KMComparator

KeYmaeraToMathematica

LiteralMathOpSpec

M2KConverter

MKComparator

MathematicaCommandRunner

MathematicaConversion

MathematicaOpSpec

MathematicaQETool

MathematicaToKeYmaera

NameMathOpSpec

NaryMathOpSpec

QuantifiedMathOpSpec

SMTConverter

UnaryMathOpSpec

Z3QETool

Z3Solver

edu.cmu.cs.ls.keymaerax.tools.qe

Z3QETool

final class Z3QETool extends Tool with QETool with ToolOperationManagement

Z3 trusted quantifier elimination tool.

See also: edu.cmu.cs.ls.keymaerax.btactics.Z3ToolProvider to obtain instances of Z3 that are properly initialized and installed/updated. Created by smitsch on 4/27/15.

Linear Supertypes

ToolOperationManagement, ToolInterface, QETool, Tool, AnyRef, Any

Ordering

Alphabetic
By Inheritance

Inherited

Z3QETool
ToolOperationManagement
ToolInterface
QETool
Tool
AnyRef
Any

Hide All
Show All

Visibility

Public
All

Instance Constructors

new Z3QETool()

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
final def asInstanceOf[T0]: T0

Definition Classes
Any
def cancel(): Boolean
Cancels the current tool operation and returns true on success, false otherwise.
Cancels the current tool operation and returns true on success, false otherwise.

Definition Classes
Z3QETool → Tool
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@native() @throws( ... )
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] )
def getAvailableWorkers: Int
<invalid inheritdoc annotation>
<invalid inheritdoc annotation>

Definition Classes
Z3QETool → ToolOperationManagement
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@native()
def getOperationTimeout: Int
Returns the timeout duration.
Returns the timeout duration.

Definition Classes
Z3QETool → ToolOperationManagement
def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@native()
def init(config: Map[String, String]): Unit
Initializes the tool with tool-specific configuration parameters.
Initializes the tool with tool-specific configuration parameters.

Definition Classes
Z3QETool → Tool
def isInitialized: Boolean
Checks whether this tool has been initialized already.
Checks whether this tool has been initialized already.

Definition Classes
Z3QETool → Tool
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
val name: String
Returns the name of the tool.
Returns the name of the tool.

Definition Classes
Z3QETool → Tool
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def notify(): Unit

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

Definition Classes
AnyRef
Annotations
@native()
def quantifierElimination(formula: Formula): Formula
Returns a quantifier-free formula that is equivalent to the specified formula.
Returns a quantifier-free formula that is equivalent to the specified formula.
formula
The formula whose quantifier-free equivalent is sought.
returns
An equivalent quantifier-free formula.

Definition Classes
Z3QETool → QETool
def restart(): Unit
Check whether the managed tool is still alive and restart it if need be.
Check whether the managed tool is still alive and restart it if need be.

Definition Classes
Z3QETool → Tool
def setOperationTimeout(timeout: Int): Unit
Sets a maximum duration of this tool's operations (e.g., QE).
Sets a maximum duration of this tool's operations (e.g., QE).

Definition Classes
Z3QETool → ToolOperationManagement
def shutdown(): Unit
Shutdown the tool
Shutdown the tool

Definition Classes
Z3QETool → Tool
final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
def toString(): String

Definition Classes
AnyRef → Any
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( ... )

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

Z3QETool

final class Z3QETool extends Tool with QETool with ToolOperationManagement

Instance Constructors

Value Members

Inherited from ToolOperationManagement

Inherited from ToolInterface

Inherited from QETool

Inherited from Tool

Inherited from AnyRef

Inherited from Any

Ungrouped

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

Z3QETool 

final class Z3QETool extends Tool with QETool with ToolOperationManagement

Instance Constructors

Value Members

Inherited from ToolOperationManagement

Inherited from ToolInterface

Inherited from QETool

Inherited from Tool

Inherited from AnyRef

Inherited from Any

Ungrouped

Z3QETool