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.
- To do
Code Review: Move non-critical tool implementations into a separate package tactictools
- Alphabetic
- By Inheritance
- Mathematica
- ToolOperationManagement
- LyapunovSolverTool
- SOSsolveTool
- PDESolverTool
- AlgebraTool
- SimplificationTool
- EquationSolverTool
- DerivativeTool
- SimulationTool
- CounterExampleTool
- ODESolverTool
- ToolInterface
- InvGenTool
- QETacticTool
- Tool
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
-
new
Mathematica(link: MathematicaLink, name: String)
- link
How to connect to the tool, either JLink or WolframScript. Created by smitsch on 4/27/15.
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
- Mathematica → Tool
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
def
deriveBy(term: Term, v: Variable): Term
Computes the symbolic partial derivative of the given term by
v
.Computes the symbolic partial derivative of the given term by
v
.d(term) ------ dv
- term
The term whose partial derivative is sought.
- v
The variable to derive by.
- returns
The partial derivative of
term
byv
.
- Definition Classes
- Mathematica → DerivativeTool
-
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
findCounterExample(formula: Formula): Option[Map[NamedSymbol, Expression]]
Returns a counterexample for the specified formula.
Returns a counterexample for the specified formula.
- formula
The formula.
- returns
A counterexample, if found. None otherwise.
- Definition Classes
- Mathematica → CounterExampleTool
-
def
genCLF(sys: List[ODESystem]): Option[Term]
Computes a Common Lyapunov Function for the switched system
sys
.Computes a Common Lyapunov Function for the switched system
sys
.- Definition Classes
- Mathematica → LyapunovSolverTool
-
def
genMLF(sys: List[ODESystem], trans: List[(Int, Int, Formula)]): List[Term]
Computes a Lyapunov function for the switched system
sys
.Computes a Lyapunov function for the switched system
sys
.- Definition Classes
- Mathematica → LyapunovSolverTool
-
def
genODECond(ode: ODESystem, assumptions: Seq[Formula], postCond: Formula): (List[Formula], List[Formula])
Returns the sufficient/necessary condition for postCond to be invariant (left of pair) also returns necessary conditions for the safety question to be true at all with those assumptions (right of pair) In either case, all formulas in the returned list must be valid
Returns the sufficient/necessary condition for postCond to be invariant (left of pair) also returns necessary conditions for the safety question to be true at all with those assumptions (right of pair) In either case, all formulas in the returned list must be valid
- Definition Classes
- Mathematica → InvGenTool
-
def
getAvailableWorkers: Int
<invalid inheritdoc annotation>
<invalid inheritdoc annotation>
- Definition Classes
- Mathematica → ToolOperationManagement
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getOperationTimeout: Int
Returns the timeout duration.
Returns the timeout duration.
- Definition Classes
- Mathematica → ToolOperationManagement
-
def
groebnerBasis(polynomials: List[Term]): List[Term]
Computes the Gröbner Basis of the given set of polynomials (with respect to some fixed monomial order).
Computes the Gröbner Basis of the given set of polynomials (with respect to some fixed monomial order). Gröbner Bases can be made unique for the fixed monomial order, when reduced, modulo scaling by constants.
- returns
The Gröbner Basis of
polynomials
. The Gröbner Basis spans the same ideal aspolynomials
but has unique remainders of polynomialReduce.
- Definition Classes
- Mathematica → AlgebraTool
- See also
polynomialReduce()
-
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
- Mathematica → Tool
-
def
invgen(ode: ODESystem, assumptions: Seq[Formula], postCond: Formula): Seq[Either[Seq[(Formula, String)], Seq[(Formula, String)]]]
Returns a continuous invariant for a safety problem sent to the tool.
Returns a continuous invariant for a safety problem sent to the tool.
- ode
The differential equation for which to generate a continuous invariants.
- assumptions
Assumptions on the initial state of the ODE.
- postCond
What to prove from the invariants.
- returns
A sequence of continuous invariants, each to be proved with a diffcut chain (left=invariant, right=candidate).
- Definition Classes
- Mathematica → InvGenTool
-
def
isInitialized: Boolean
Checks whether this tool has been initialized already.
Checks whether this tool has been initialized already.
- Definition Classes
- Mathematica → Tool
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
lzzCheck(ode: ODESystem, inv: Formula): Boolean
Fast check whether or not
inv
is worth proving to be an invariant ofode
.Fast check whether or not
inv
is worth proving to be an invariant ofode
.- Definition Classes
- Mathematica → InvGenTool
-
val
name: String
Returns the name of the tool.
Returns the name of the tool.
- Definition Classes
- Mathematica → 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
odeSolve(diffSys: DifferentialProgram, diffArg: Variable, iv: Map[Variable, Variable]): Option[Formula]
Returns a formula describing the symbolic solution of the specified differential equation system.
Returns a formula describing the symbolic solution of the specified differential equation system.
- diffSys
The differential equation system
- diffArg
The independent variable of the ODE, usually time
- iv
Names of initial values per variable, e.g., x -> x_0
- returns
The solution, if found. None otherwise.
- Definition Classes
- Mathematica → ODESolverTool
-
def
pdeSolve(diffSys: DifferentialProgram): Iterator[Term]
Computes the symbolic solution of the inverse characteristic partial differential equation corresponding to an ordinary differential equation.
Computes the symbolic solution of the inverse characteristic partial differential equation corresponding to an ordinary differential equation.
- diffSys
The system of differential equations of the form x'=theta,y'=eta.
- returns
A list of solutions for
f
of the inverse characteristic PDEtheta*df/dx + eta*df/dy = 0
if found.
- Definition Classes
- Mathematica → PDESolverTool
-
def
polynomialReduce(polynomial: Term, GB: List[Term]): (List[Term], Term)
Computes the multivariate polynomial reduction of
polynomial
divided with respect to the set of polynomialsGB
, which is guaranteed to be unique iffGB
is a Gröbner basis.Computes the multivariate polynomial reduction of
polynomial
divided with respect to the set of polynomialsGB
, which is guaranteed to be unique iffGB
is a Gröbner basis. Returns the list of cofactors and the remainder. Repeatedly divides the leading term ofpolynomial
by a corresponding multiple of a polynomial ofGB
while possible. Each individual reduction divides the leading term ofpolynomial
by the required multiple of the leading term of the polynomial ofGB
such that those cancel. Let l(p) be the leading monomial of p and lc(p) its leading coefficient. Then each round of reduction of p:=polynomial with leading terml*X^v
picks a polynomial g in
GBand turns it into
p := p - l/lc(g) * X^v/l(g) * g
alias
p := p - (l/(lc(g) * l(g)))*X^v * g
The former leading monomial
X^v
no longer occurs in the resulting polynomial and
pgot smaller or is now 0. To determine leading terms, polynomial reduction uses the same fixed monomial order that groeberBasis() uses. The remainders will be unique (independent of the order of divisions) iff
GBis a Gröbner Basis.
- polynomial
the multivariate polynomial to divide by the elements of
GB
until saturation.- GB
the set of multivariate polynomials that
polynomial
will repeatedly be divided by. The result of this algorithm is particularly insightful (and has unique remainders) ifGB
is a Gröbner Basis.- returns
(coeff, rem) where
rem
is the result of multivariate polynomial division ofpolynomial
byGB
andcoeff
are the respective coefficients of the polynomials inGB
that explain the result. That ispolynomial == coeff(1)*GB(1) + coeff(2)*GB(2) + ... + coeff(n)*GB(n) + rem
alias
rem == polynomial - coeff(1)*GB(1) - coeff(2)*GB(2) - ... - coeff(n)*GB(n)
In addition, the remainder
rem
is small in that its leading monomial cannot be divided by leading monomials of any polynomial inGB
. The resultrem
is unique whenGB
is a Gröbner Basis.
- Definition Classes
- Mathematica → AlgebraTool
polynomialReduce("y^3 + 2*x^2*y".asTerm, List("x^2-y".asTerm, "y^2+5".asTerm)) = ((2*y :: 2 + y), -5*y-10) // because y^3 + 2*x^2*y == (2*y) * (x^2-y) + (2+y) * (y^2+5) + (-5*y-10)
- See also
groebnerBasis()
Example: -
def
qe(goal: Goal, continueOnFalse: Boolean): (Goal, Formula)
Returns the result of the first-to-finish (sub-)goal in
g
(result of the first-to-finish sub-goal of OneOf, else result of Atom or AllOf).Returns the result of the first-to-finish (sub-)goal in
g
(result of the first-to-finish sub-goal of OneOf, else result of Atom or AllOf). WhencontinueOnFalse
is set, continues trying other options in case a finished option's result is false.- Definition Classes
- Mathematica → QETacticTool
-
def
qe(formula: Formula): Lemma
Quantifier elimination on the specified formula, returns an equivalent quantifier-free formula plus Mathematica input/output as evidence
Quantifier elimination on the specified formula, returns an equivalent quantifier-free formula plus Mathematica input/output as evidence
- formula
The formula whose quantifier-free equivalent is sought.
- returns
A lemma showing equivalence between
formula
and a quantifier-free formula, with tool evidence.
- Definition Classes
- Mathematica → QETacticTool
-
def
quotientRemainder(term: Term, div: Term, x: Variable): (Term, Term)
Computes the quotient and remainder of
term
divided bydiv
.Computes the quotient and remainder of
term
divided bydiv
.- term
the polynomial term to divide, considered as a univariate polynomial in variable
v
with coefficients that may have other variables.- div
the polynomial term to divide
term
by, considered as a univariate polynomial in variablev
with coefficients that may have other variables.
- Definition Classes
- Mathematica → AlgebraTool
quotientRemainder("6*x^2+4*x+8".asTerm, "2*x".asTerm, Variable("x")) == (3*x+2, 8) // because (6*x^2+4*x+8) == (3*x+2) * (2*x) + 8 // so the result of division is 3*x+2 with remainder 8
Example: -
def
refuteODE(ode: ODESystem, assumptions: Seq[Formula], postCond: Formula): Option[Map[NamedSymbol, Expression]]
Finds counterexamples to an ODE safety conjecture.
Finds counterexamples to an ODE safety conjecture.
- Definition Classes
- Mathematica → InvGenTool
-
def
restart(): Unit
Restarts the MathKernel with the current configuration
Restarts the MathKernel with the current configuration
- Definition Classes
- Mathematica → 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
- Mathematica → ToolOperationManagement
-
def
shutdown(): Unit
Closes the connection to Mathematica
Closes the connection to Mathematica
- Definition Classes
- Mathematica → Tool
-
def
simplify(expr: Term, assumptions: List[Formula]): Term
- Definition Classes
- Mathematica → SimplificationTool
-
def
simplify(expr: Formula, assumptions: List[Formula]): Formula
- Definition Classes
- Mathematica → SimplificationTool
-
def
simplify(expr: Expression, assumptions: List[Formula]): Expression
Simplifies the given expression
expr
, under the list of assumptions.Simplifies the given expression
expr
, under the list of assumptions.- expr
The formula or term to simplify.
- assumptions
The list of logical formulas whose conjunction is assumed to hold during the simplification. The assumptions are allowed to contain additional conjunctions.
- returns
A simplified version of
expr
.
- Definition Classes
- Mathematica → SimplificationTool
simplify("a*x^2+b^2 > a*x^3+b*abs(b)".asFormula, "x>1".asFormula :: "b>0".asFormula::Nil) == "a<0".asFormula simplify("a*x^2+b^2 > a*x^3+b*abs(b)".asFormula, "x>1 && b>0".asFormula::Nil) == "a<0".asFormula
Example: -
def
simulate(initial: Formula, stateRelation: Formula, steps: Int = 10, n: Int = 1): Simulation
Returns a list of simulated states, where consecutive states in the list satisfy 'stateRelation'.
Returns a list of simulated states, where consecutive states in the list satisfy 'stateRelation'. The state relation is a modality-free first-order formula. The simulation starts in a state where initial holds (first-order formula).
- initial
A first-order formula describing the initial state.
- stateRelation
A first-order formula describing the relation between consecutive states. The relationship is by name convention: postfix 'pre': prior state; no postfix: posterior state.
- steps
The length of the simulation run (i.e., number of states).
- n
The number of simulations (different initial states) to create.
- returns
'n' lists (length 'steps') of simulated states.
- Definition Classes
- Mathematica → SimulationTool
-
def
simulateRun(initial: SimState, stateRelation: Formula, steps: Int = 10): SimRun
Returns a list of simulated states, where consecutive states in the list satisfy 'stateRelation'.
Returns a list of simulated states, where consecutive states in the list satisfy 'stateRelation'. The state relation is a modality-free first-order formula. The simulation starts in the specified initial state.
- initial
The initial state: concrete values .
- stateRelation
A first-order formula describing the relation between consecutive states. The relationship is by name convention: postfix 'pre': prior state; no postfix: posterior state.
- steps
The length of the simulation run (i.e., number of states).
- returns
A list (length 'steps') of simulated states.
- Definition Classes
- Mathematica → SimulationTool
-
def
solve(equations: Formula, vars: List[Expression]): Option[Formula]
Computes the symbolic solution of an equation system written as a conjunction of equations.
Computes the symbolic solution of an equation system written as a conjunction of equations.
- equations
The system of equations as a conjunction of equations.
- vars
The variables or symbols to solve for. Within reason, it may also be possible to solve for compound expressions like solve for j(z).
- returns
The solution if found; None otherwise The solution should be a conjunction of explicit equations for the vars. Or a disjunction of a conjunction of explicit equations for the vars.
- Definition Classes
- Mathematica → EquationSolverTool
solve("z+1=3&x+5=z-1".asFormula, Variable("z")::Variable("x")::Nil) == Some("z=2&x=-4")
Example: -
def
sosSolve(polynomials: List[Term], variables: List[Term], degree: Int, timeout: Option[Int]): Result
Returns a continuous invariant for a safety problem sent to the tool.
Returns a continuous invariant for a safety problem sent to the tool.
- returns
(1 + sos, cofactors) such that (cofactors, polynomials).zipped.map(Times) = 1 + sos.
- Definition Classes
- Mathematica → SOSsolveTool
-
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( ... )
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