package tools
Arithmetic backends and arithmetic utilities for tactics, including an SMT interface.
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.edu.cmu.cs.ls.keymaerax.tools.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

trait
AlgebraTool extends ToolInterface
Tool for computer algebraic computations.
Tool for computer algebraic computations.

abstract
class
BaseKeYmaeraMathematicaBridge[T] extends KeYmaeraMathematicaBridge[T]
Base class for Mathematica bridges.
Base class for Mathematica bridges. Running commands is synchronized.
 class ConversionException extends Exception

trait
CounterExampleTool extends ToolInterface
Quantifier elimination tool.
Quantifier elimination tool.

trait
DerivativeTool extends ToolInterface
Tool for computing symbolic derivatives (oracle for tactics).

trait
EquationSolverTool extends ToolInterface
Tool for computing the solution of an equation system.
Tool for computing the solution of an equation system.
 case class HashEvidence(h: String) extends Evidence with Product with Serializable

class
JLinkMathematicaLink extends MathematicaLink with Logging
A link to Mathematica using the JLink interface.

trait
K2MConverter[T] extends (T) ⇒ MExpr
Converts KeYmaera > Mathematica
Converts KeYmaera > Mathematica
 T
usually Expression, but also other source types for nonsoundnesscritical conversions.

class
KMComparator extends AnyRef
Compares Mathematica expressions for equality (handles conversion differences).

trait
KeYmaeraMathematicaBridge[T] extends AnyRef
Bridge for MathematicaLink, bundles tool executor (thread pools) with converters.
 class KeYmaeraToMathematica extends K2MConverter[KExpr]

trait
M2KConverter[T] extends (MExpr) ⇒ T
Converts Mathematica > KeYmaera
Converts Mathematica > KeYmaera
 T
usually Expression, but also other target types for nonsoundnesscritical conversions.
 class MKComparator[T] extends AnyRef

class
Mathematica extends ToolBase with QETool with InvGenTool with ODESolverTool with CounterExampleTool with SimulationTool with DerivativeTool with EquationSolverTool with SimplificationTool with AlgebraTool with PDESolverTool with ToolOperationManagement
Mathematica tool for quantifier elimination and solving differential equations.
Mathematica tool for quantifier elimination and solving differential equations.
Created by smitsch on 4/27/15.
 To do
Code Review: Move noncritical tool implementations into a separate package tactictools

class
MathematicaAlgebraTool extends BaseKeYmaeraMathematicaBridge[KExpr] with AlgebraTool
A link to Mathematica using the JLink interface.

class
MathematicaCEXTool extends BaseKeYmaeraMathematicaBridge[KExpr] with CounterExampleTool with Logging
Mathematica counter example implementation.

class
MathematicaComputationAbortedException extends ConversionException
Internal abort of computations (e.g., by TimeConstrained).

class
MathematicaComputationExternalAbortException extends ConversionException
Externally triggered abort (e.g., by stopping from the UI).
 class MathematicaComputationFailedException extends ConversionException

class
MathematicaEquationSolverTool extends BaseKeYmaeraMathematicaBridge[KExpr] with EquationSolverTool
A link to Mathematica using the JLink interface.

class
MathematicaInvGenTool extends BaseKeYmaeraMathematicaBridge[KExpr] with InvGenTool with Logging
A continuous invariant implementation using Mathematica over the JLink interface.

trait
MathematicaLink extends AnyRef
An abstract interface to Mathematica link implementations.
An abstract interface to Mathematica link implementations. The link may be used synchronously or asychronously. Multiple MathematicaLinks may be created by instantiating multiple copies of implementing classes (depends on license).

class
MathematicaODESolverTool extends BaseKeYmaeraMathematicaBridge[KExpr] with ODESolverTool with DerivativeTool
A link to Mathematica using the JLink interface.

class
MathematicaPDESolverTool extends BaseKeYmaeraMathematicaBridge[KExpr] with PDESolverTool
A link to Mathematica using the JLink interface.

class
MathematicaQETool extends BaseKeYmaeraMathematicaBridge[KExpr] with QETool with Logging
A QE tool implementation using Mathematica over the JLink interface.

class
MathematicaSimplificationTool extends BaseKeYmaeraMathematicaBridge[KExpr] with SimplificationTool
A link to Mathematica using the JLink interface.

class
MathematicaSimulationTool extends BaseKeYmaeraMathematicaBridge[Simulation] with SimulationTool
A link to Mathematica using the JLink interface.
 class MathematicaToKeYmaera extends M2KConverter[KExpr]
 class NoCountExException extends Exception

trait
ODESolverTool extends ToolInterface
Tool for computing the symbolic solution of a differential equation system.
Tool for computing the symbolic solution of a differential equation system.

trait
PDESolverTool extends ToolInterface
Tool for computing the symbolic solution of a partial differential equation system.
Tool for computing the symbolic solution of a partial differential equation system.

class
Polya extends ToolBase with QETool
Polya quantifier elimination tool.
Polya quantifier elimination tool.
Created by smitsch on 4/27/15.

class
PolyaSolver extends SMTSolver with Logging
Created by ran on 4/24/15.
 class SMTConversionException extends ConversionException

abstract
class
SMTConverter extends (Formula) ⇒ String with Logging
Base class for SMT converters with conversion per SMTLib specification.
Base class for SMT converters with conversion per SMTLib specification. Created by ran on 8/24/15.
 class SMTQeException extends Exception

trait
SMTSolver extends QETool
Common interface for SMT solvers.

trait
SimplificationTool extends ToolInterface
Tool for simplifying logical and/or arithmetical expressions.
Tool for simplifying logical and/or arithmetical expressions.

trait
SimulationTool extends ToolInterface
Simulation tool.
Simulation tool.

class
TestSynthesis extends BaseKeYmaeraMathematicaBridge[KExpr]
Synthesize test case configurations from ModelPlex formulas.
Synthesize test case configurations from ModelPlex formulas. Requires Mathematica.
Created by smitsch on 12/6/16.

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.

abstract
class
ToolBase extends Tool
Base class for tool instances (e.g., a specific mathematica kernel)
 case class ToolEvidence(info: List[(String, String)]) extends Evidence with Product with Serializable

case class
ToolException(msg: String, cause: Throwable = null) extends ProverException with Product with Serializable
Arithmetic tool exceptions
 class ToolExecutor[T] extends Logging

trait
ToolInterface extends AnyRef
Base trait tagging interfaces to tools.

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
 class UncheckedK2MConverter extends KeYmaeraToMathematica
 class UncheckedM2KConverter extends MathematicaToKeYmaera

class
Z3 extends ToolBase with QETool with ToolOperationManagement
Z3 quantifier elimination tool.
Z3 quantifier elimination tool.
Created by smitsch on 4/27/15.

class
Z3Solver extends ToolOperationManagementBase with SMTSolver with Logging
Created by ran on 3/27/15.
Value Members

def
diagnostic: String
Gather diagnostic information about the system configuration relevant to KeYmaera X and its tool integrations.
 object CEXK2MConverter extends UncheckedK2MConverter
 object CEXM2KConverter extends UncheckedM2KConverter

object
DefaultSMTConverter extends SMTConverter
A default SMT converter with output as preferred by KeYmaera X.
 object DiffUncheckedM2KConverter

object
KMComparator
Implicit conversion from Mathematica expressions to comparator.

object
KeYmaeraToMathematica extends KeYmaeraToMathematica
Converts KeYmaeara X expression data structures to Mathematica Expr objects.

object
KeYmaeraXTool extends ToolBase
The KeYmaera X tool.
The KeYmaera X tool.
Created by smitsch on 4/27/15.

object
MKComparator
Implicit conversion from KeYmaera expressions to comparator.

object
MathematicaConversion
Mathematica conversion stuff.

object
MathematicaToKeYmaera extends MathematicaToKeYmaera
Converts com.wolfram.jlink.Expr > edu.cmu...keymaerax.core.Expr
 object PegasusM2KConverter extends UncheckedM2KConverter
 object SimulationK2MConverter extends K2MConverter[Simulation]
 object SimulationM2KConverter extends M2KConverter[Simulation]
 object SimulationTool
Deprecated Value Members

object
ToolConversions
 Annotations
 @deprecated
 Deprecated
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 structuresedu.cmu.cs.ls.keymaerax.core.Expression
 Differential dynamic logic expressionsedu.cmu.cs.ls.keymaerax.core.Sequent
 Sequents of formulasedu.cmu.cs.ls.keymaerax.core.Rule
 Proof rulesedu.cmu.cs.ls.keymaerax.core.Provable
 Proof certificateedu.cmu.cs.ls.keymaerax.btactics
 Tactic language libraryedu.cmu.cs.ls.keymaerax.btactics.TactixLibrary
 Main tactic libraryedu.cmu.cs.ls.keymaerax.btactics.HilbertCalculus
 Hilbert Calculus for differential dynamic logicedu.cmu.cs.ls.keymaerax.btactics.SequentCalculus
 Sequent Calculus for propositional and firstorder logicedu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus
 Unificationbased Uniform Substitution Calculusedu.cmu.cs.ls.keymaerax.bellerophon
 Bellerophon tactic language and tactic interpreteredu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr
 Tactic language expressionsedu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter
 Sequential tactic interpreteredu.cmu.cs.ls.keymaerax.parser
 Parser and pretty printer with concrete syntax and notation for differential dynamic logic.edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser
 Parser for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter
 Pretty printer for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXProblemParser
 Parser for KeYmaera X problem files.kyx
edu.cmu.cs.ls.keymaerax.lemma
 Lemma mechanismedu.cmu.cs.ls.keymaerax.lemma.FileLemmaDB
 Lemma database stored in filesedu.cmu.cs.ls.keymaerax.tools
 Arithmetic backendsedu.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
 Commandline launcher for KeYmaera X supports commandline argumenthelp
to obtain usage informationedu.cmu.cs.ls.keymaerax.btactics.DerivationInfo
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface info.References
Full references are provided elsewhere 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. 219265, 2017.
2. Nathan Fulton, Stefan Mitsch, JanDavid 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, LNCS. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.