class MathematicaAlgebraTool extends BaseKeYmaeraMathematicaBridge[KExpr] with AlgebraTool
A link to Mathematica using the JLink interface.
- Alphabetic
- By Inheritance
- MathematicaAlgebraTool
- AlgebraTool
- ToolInterface
- BaseKeYmaeraMathematicaBridge
- KeYmaeraMathematicaBridge
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new MathematicaAlgebraTool(link: MathematicaLink)
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
-
val
DEBUG: Boolean
- Attributes
- protected
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
val
MEMORY_LIMIT_OFF: Long
Default memory limit: no limit.
Default memory limit: no limit.
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
val
TIMEOUT_OFF: Int
Default timeout for Mathematica requests: no timeout.
Default timeout for Mathematica requests: no timeout.
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
availableWorkers: Int
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
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] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
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 aspolynomialsbut has unique remainders of polynomialReduce.
- Definition Classes
- MathematicaAlgebraTool → AlgebraTool
- See also
polynomialReduce()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
init(): Boolean
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
val
k2m: K2MConverter[KExpr]
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
val
link: MathematicaLink
- Definition Classes
- MathematicaAlgebraTool → BaseKeYmaeraMathematicaBridge
-
val
m2k: M2KConverter[KExpr]
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
var
mathematicaExecutor: ToolExecutor
- Attributes
- protected
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
def
memoryConstrained(cmd: String): String
- Attributes
- protected
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
def
memoryConstrained(cmd: MExpr): MExpr
- Attributes
- protected
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
var
memoryLimit: Long
Memory limit for Mathematica requests in MB, set to MEMORY_LIMIT_OFF to disable.
Memory limit for Mathematica requests in MB, set to MEMORY_LIMIT_OFF to disable.
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
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
polynomialReduce(polynomial: Term, GB: List[Term]): (List[Term], Term)
Computes the multivariate polynomial reduction of
polynomialdivided with respect to the set of polynomialsGB, which is guaranteed to be unique iffGBis a Gröbner basis.Computes the multivariate polynomial reduction of
polynomialdivided with respect to the set of polynomialsGB, which is guaranteed to be unique iffGBis a Gröbner basis. Returns the list of cofactors and the remainder. Repeatedly divides the leading term ofpolynomialby a corresponding multiple of a polynomial ofGBwhile possible. Each individual reduction divides the leading term ofpolynomialby the required multiple of the leading term of the polynomial ofGBsuch 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^vpicks a polynomial g inGBand turns it intop := 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^vno longer occurs in the resulting polynomial andpgot 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) iffGBis a Gröbner Basis.- polynomial
the multivariate polynomial to divide by the elements of
GBuntil saturation.- GB
the set of multivariate polynomials that
polynomialwill repeatedly be divided by. The result of this algorithm is particularly insightful (and has unique remainders) ifGBis a Gröbner Basis.- returns
(coeff, rem) where
remis the result of multivariate polynomial division ofpolynomialbyGBandcoeffare the respective coefficients of the polynomials inGBthat 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
remis small in that its leading monomial cannot be divided by leading monomials of any polynomial inGB. The resultremis unique whenGBis a Gröbner Basis.
- Definition Classes
- MathematicaAlgebraTool → 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
quotientRemainder(term: Term, div: Term, x: Variable): (Term, Term)
Computes the quotient and remainder of
termdivided bydiv.Computes the quotient and remainder of
termdivided bydiv.- term
the polynomial term to divide, considered as a univariate polynomial in variable
vwith coefficients that may have other variables.- div
the polynomial term to divide
termby, considered as a univariate polynomial in variablevwith coefficients that may have other variables.
- Definition Classes
- MathematicaAlgebraTool → 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
run(cmd: MExpr): (String, KExpr)
Runs Mathematica command
cmd, with Mathematica exception checking.Runs Mathematica command
cmd, with Mathematica exception checking.- Definition Classes
- BaseKeYmaeraMathematicaBridge → KeYmaeraMathematicaBridge
-
def
runUnchecked(cmd: String): (String, KExpr)
Runs Mathematica command
cmdwithout safeguarding by exception checking for Mathematica results.Runs Mathematica command
cmdwithout safeguarding by exception checking for Mathematica results.- Definition Classes
- BaseKeYmaeraMathematicaBridge → KeYmaeraMathematicaBridge
-
def
shutdown(): Unit
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
timeConstrained(cmd: String): String
- Attributes
- protected
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
def
timeConstrained(cmd: MExpr): MExpr
- Attributes
- protected
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
var
timeout: Int
Timeout for Mathematica requests in seconds, set to TIMEOUT_OFF to disable.
Timeout for Mathematica requests in seconds, set to TIMEOUT_OFF to disable.
- Definition Classes
- BaseKeYmaeraMathematicaBridge
-
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,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