trait AlgebraTool extends ToolInterface
Tool for computer algebraic computations.
 Alphabetic
 By Inheritance
 AlgebraTool
 ToolInterface
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Abstract Value Members

abstract
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.

abstract
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.
polynomialReduce("y^3 + 2*x^2*y".asTerm, List("x^2y".asTerm, "y^2+5".asTerm)) = ((2*y :: 2 + y), 5*y10) // because y^3 + 2*x^2*y == (2*y) * (x^2y) + (2+y) * (y^2+5) + (5*y10)
 See also
groebnerBasis()
Example: 
abstract
def
quotientRemainder(term: Term, div: Term, v: 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. v
the variable with respect to which
term
anddiv
are regarded as univariate polynomials (with coefficients that may have other variables).
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:
Concrete 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
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
hashCode(): Int
 Definition Classes
 AnyRef → Any
 Annotations
 @native()

final
def
isInstanceOf[T0]: Boolean
 Definition Classes
 Any

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()

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 (onepass) 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 firstorder logicHybridProgramCalculus
 Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
 Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
 Unificationbased 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 backend solversMathematicaQETool
 Mathematica interface for real arithmetic.Z3QETool
 Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext
 Extended backends 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
 Commandline launcher for KeYmaera X supports commandline argumenthelp
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
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface 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. 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, volume 9195 of LNCS, pp. 527538. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018. Videos