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.
- To do
Stub. Describe for real.
- Alphabetic
- By Inheritance
- tools
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
case class
ConversionException(msg: String, cause: Throwable = null) extends ToolInternalException with Product with Serializable
Reports internal errors converting to/from a tool.
-
case class
MathematicaComputationAbortedException(msg: String, cause: Throwable = null) extends ToolExternalException with Product with Serializable
Abort of external computations (e.g., by TimeConstrained, by $Abort).
-
case class
MathematicaComputationFailedException(msg: String, cause: Throwable = null) extends ToolExternalException with Product with Serializable
Reports external Mathematica computation failures ($Failed).
-
case class
MathematicaComputationUserAbortException(msg: String) extends ToolInternalException with Product with Serializable
User-triggered abort (e.g., by stopping from the UI).
-
case class
MathematicaInapplicableMethodException(msg: String, cause: Throwable = null) extends ToolExternalException with Product with Serializable
Abort of external computation due to inapplicable methods.
-
case class
MathematicaMathlinkException(msg: String, cause: Throwable = null) extends ToolCriticalException with Product with Serializable
Critical Mathlink errors that require restarting Mathematica.
-
case class
MathematicaUnknownCauseCriticalException(msg: String) extends ToolCriticalException with Product with Serializable
Critical Mathematica exceptions that require restarting due to unknown external cause.
-
case class
SMTQeException(msg: String, cause: Throwable = null) extends ToolExternalException with Product with Serializable
Reports QE errors from Z3.
-
case class
SMTTimeoutException(msg: String, cause: Throwable = null) extends ToolInternalException with Product with Serializable
Reports timeouts from Z3.
-
trait
Tool extends AnyRef
Defines the lifecycle for external tools.
Defines the lifecycle for external tools. A tool is available once init is called. It cannot be used after shutdown. For intermediate restarting, use check_and_recover.
-
case class
ToolCommunicationException(msg: String, cause: Throwable = null) extends ToolInternalException with Product with Serializable
Internal errors when setting up tools, communicating commands, etc.
-
abstract
class
ToolCriticalException extends ToolException
Critical errors requiring the external tool or even KeYmaera X to be restarted.
-
case class
ToolEvidence(info: List[(String, String)]) extends Evidence with Product with Serializable
Evidence provided by tools.
-
abstract
class
ToolException extends ProverException
Tool exceptions.
-
case class
ToolExecutionException(msg: String, cause: Throwable = null) extends ToolExternalException with Product with Serializable
External execution errors when setting up tool, starting, executing commands, shutdown etc.
-
abstract
class
ToolExternalException extends ToolException
Errors raised from the external tool.
-
trait
ToolInterface extends AnyRef
Base trait tagging interfaces to tools.
-
abstract
class
ToolInternalException extends ToolException
Errors raised from the KeYmaera X side of the tool interaction.
-
trait
ToolOperationManagement extends ToolInterface
Manages how a tool's operations work (e.g., timeouts).
-
abstract
class
ToolOperationManagementBase extends ToolOperationManagement
Base class for tool operation management
Value Members
-
def
diagnostic: String
Gather diagnostic information about the system configuration relevant to KeYmaera X and its tool integrations.
-
object
KeYmaeraXTool extends Tool
The KeYmaera X tool, initializes the pretty printer.
The KeYmaera X tool, initializes the pretty printer.
Created by smitsch on 4/27/15.
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 structuresExpression
- Differential dynamic logic expressions:Term
,Formula
,Program
Sequent
- Sequents of formulasProvable
- Proof certificates transformed by rules/axiomsRule
- Proof rules as well asUSubstOne
for (one-pass) uniform substitutions and renaming.StaticSemantics
- Static semantics with free and bound variable analysisKeYmaeraXParser
.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 syntaxKeYmaeraXParser
- Parser reading concrete KeYmaera X syntaxKeYmaeraXArchiveParser
- Parser reading KeYmaera X model and proof archive.kyx
filesDLParser
- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser
- Combinator parser reading KeYmaera X model and proof archive.kyx
filesedu.cmu.cs.ls.keymaerax.infrastruct
- Prover infrastructure outside the kernelUnificationMatch
- Unification algorithmRenUSubst
- 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 functionalityExpressionTraversal
- Generic traversal functionality for expressionsedu.cmu.cs.ls.keymaerax.bellerophon
- Bellerophon tactic language and tactic interpreterBelleExpr
- Tactic language expressionsSequentialInterpreter
- Sequential tactic interpreter for Bellerophon tacticsedu.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 logicSequentCalculus
- Sequent Calculus for propositional and first-order logicHybridProgramCalculus
- Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
- Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
- 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 conclusionsedu.cmu.cs.ls.keymaerax.lemma
- Lemma mechanismLemma
- 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 solversMathematicaQETool
- 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 informationedu.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