package ext
- Alphabetic
- Public
- All
Type Members
-
trait
AlgebraTool extends ToolInterface
Tool for computer algebraic computations.
Tool for computer algebraic computations.
-
case class
AllOf(goals: Seq[Goal]) extends Goal with Product with Serializable
All of the goals must be proved.
-
case class
Atom(goal: Formula) extends Goal with Product with Serializable
A single formula.
-
abstract
class
BaseKeYmaeraMathematicaBridge[T] extends KeYmaeraMathematicaBridge[T]
Base class for Mathematica bridges.
Base class for Mathematica bridges. Running commands is synchronized.
-
final
class
BigDecimalTool extends Tool with QETacticTool with ToolOperationManagement
Big decimal quantifier elimination tool for tactics, forwards to BigDecimalQETool.
-
trait
CounterExampleTool extends ToolInterface
Counterexample generation tool for first-order real arithmetic formulas.
Counterexample generation tool for first-order real arithmetic formulas.
-
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.
-
trait
Goal extends AnyRef
Goals for parallel QE execution.
-
class
JLinkMathematicaLink extends MathematicaLink with Logging
A link to Mathematica using the JLink interface.
-
trait
KeYmaeraMathematicaBridge[T] extends AnyRef
Bridge for MathematicaLink, bundles tool executor (thread pools) with converters.
-
trait
LyapunovSolverTool extends ToolInterface
Tool for computing Lyapunov functions.
-
class
Mathematica extends Tool with QETacticTool with InvGenTool with ODESolverTool with CounterExampleTool with SimulationTool with DerivativeTool with EquationSolverTool with SimplificationTool with AlgebraTool with PDESolverTool with SOSsolveTool with LyapunovSolverTool with ToolOperationManagement
Mathematica/Wolfram Engine tool for quantifier elimination and solving differential equations.
Mathematica/Wolfram Engine tool for quantifier elimination and solving differential equations.
- To do
Code Review: Move non-critical 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[Either[KExpr, NamedSymbol]] with CounterExampleTool with Logging
Mathematica counter example implementation.
-
class
MathematicaEquationSolverTool extends BaseKeYmaeraMathematicaBridge[KExpr] with EquationSolverTool
A link to Mathematica using the JLink interface.
-
class
MathematicaInvGenTool extends BaseKeYmaeraMathematicaBridge[Expression] 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 MathematicaLyapunovSolverTool extends BaseKeYmaeraMathematicaBridge[KExpr] with LyapunovSolverTool
-
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
MathematicaQEToolBridge[T] extends BaseKeYmaeraMathematicaBridge[T]
Asynchronous bridge to edu.cmu.cs.ls.keymaerax.tools.qe.MathematicaQETool.
-
class
MathematicaSOSsolveTool extends BaseKeYmaeraMathematicaBridge[Expression] with SOSsolveTool with Logging
Link to Yong Kiams SOSsolve implementation in 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.
-
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.
-
case class
OneOf(goals: Seq[Goal]) extends Goal with Product with Serializable
One of the goals must be proved.
-
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.
-
trait
QETacticTool extends AnyRef
Quantifier elimination tool that combines trusted edu.cmu.cs.ls.keymaerax.core.QETool with other untrusted tools (so that tools implementing QETacticTool can forward to a trusted edu.cmu.cs.ls.keymaerax.core.QETool without being trusted themselves).
- class RingsAlgebraTool extends Tool with AlgebraTool
-
class
RingsLibrary extends AnyRef
A link to Rings library for its algebra tools
- trait SOSsolveTool extends AnyRef
-
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
SmlQEPrinter extends AnyRef
Prints expressions to SML QE data structure.
-
class
TestSynthesis extends BaseKeYmaeraMathematicaBridge[Either[KExpr, NamedSymbol]]
Synthesize test case configurations from ModelPlex formulas.
Synthesize test case configurations from ModelPlex formulas. Requires Mathematica.
Created by smitsch on 12/6/16.
-
class
ToolExecutor extends Logging
A tool executor executes commands concurrently on up to
poolSizethreads. - class UncheckedBaseK2MConverter extends KeYmaeraToMathematica
- class UncheckedBaseM2KConverter extends MathematicaToKeYmaera
-
class
WolframScript extends MathematicaLink with Logging
A link to Wolfram Engine via WolframScript.
-
final
class
Z3 extends Tool with QETacticTool with SimplificationTool with ToolOperationManagement
Z3 quantifier elimination tool for tactics.
Z3 quantifier elimination tool for tactics.
- See also
edu.cmu.cs.ls.keymaerax.btactics.Z3ToolProvider to obtain instances of Z3 that are properly initialized and installed/updated.
Value Members
- object CEXK2MConverter extends K2MConverter[Either[KExpr, NamedSymbol]]
- object CEXM2KConverter extends M2KConverter[Either[KExpr, NamedSymbol]]
- object DiffUncheckedM2KConverter
-
object
ExtMathematicaOpSpec
Extended Mathematica operator specifications for non-soundness critical tools.
- object IdentityConverter extends M2KConverter[MExpr]
- object PegasusK2MConverter extends UncheckedBaseK2MConverter
- object PegasusM2KConverter extends UncheckedBaseM2KConverter with Logging
- object PlotConverter extends UncheckedBaseK2MConverter
- object SOSsolveTool
- object SimulationK2MConverter extends K2MConverter[Simulation]
- object SimulationM2KConverter extends M2KConverter[Simulation]
-
object
SimulationTool
Simulation tool types.
-
object
SmlQENoRoundingPrinter extends (Formula) ⇒ String
Prints SML QE problems with RatReal, avoiding rounding.
-
object
SmlQEReal64Printer extends (Formula) ⇒ String
Prints SML QE problems with Real64 rounding.
-
object
SmtLibReader
Reads Expressions from SMT-LIB format: converts every (assert X) statement into an expression.
- object UncheckedBaseConverter
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,ProgramSequent- Sequents of formulasProvable- Proof certificates transformed by rules/axiomsRule- Proof rules as well asUSubstOnefor (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.kyxfilesDLParser- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser- Combinator parser reading KeYmaera X model and proof archive.kyxfilesedu.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-helpto 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