object UnificationMatch extends FreshUnificationMatch
Unification/matching algorithm for tactics.
Unify(shape, input)
matches second argument input
against the pattern shape
of the first argument but not vice versa.
Matcher leaves input
alone and only substitutes into shape
, i.e., gives a singlesided matcher.
 See also
 Alphabetic
 By Inheritance
 UnificationMatch
 FreshUnificationMatch
 SchematicComposedUnificationMatch
 SchematicUnificationMatch
 BaseMatcher
 Logging
 LazyLogging
 LoggerHolder
 Matcher
 Function2
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Type Members

type
Subst = RenUSubst
The (generalized) substitutions used for unification purposes

type
SubstRepl = (Expression, Expression)
A (generalized) substitution pair, which is either like a SubstitutionPair for uniform substitution or a pair of Variable for uniform renaming.
A (generalized) substitution pair, which is either like a SubstitutionPair for uniform substitution or a pair of Variable for uniform renaming.
 Definition Classes
 Matcher
 See also
SubstitutionPair
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

def
Subst(subs: List[SubstRepl]): Subst
Create a (generalized) substitution from the given representation
subs
.Create a (generalized) substitution from the given representation
subs
. Faster since compose preserves distinctness. Attributes
 protected
 Definition Classes
 FreshUnificationMatch → Matcher

def
SubstRepl(what: Expression, repl: Expression): SubstRepl
Create a (generalized) substitution pair.
Create a (generalized) substitution pair.
 Attributes
 protected
 Definition Classes
 Matcher
 See also
SubstitutionPair

def
apply(e1: Sequent, e2: Sequent): Subst
apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
.apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
. Definition Classes
 BaseMatcher → Matcher
 Exceptions thrown
UnificationException
ifinput
cannot be matched against the patternshape
.

def
apply(e1: DifferentialProgram, e2: DifferentialProgram): Subst
apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
.apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
. Definition Classes
 BaseMatcher → Matcher
 Exceptions thrown
UnificationException
ifinput
cannot be matched against the patternshape
.

def
apply(e1: Program, e2: Program): Subst
apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
.apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
. Definition Classes
 BaseMatcher → Matcher
 Exceptions thrown
UnificationException
ifinput
cannot be matched against the patternshape
.

def
apply(e1: Formula, e2: Formula): Subst
apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
.apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
. Definition Classes
 BaseMatcher → Matcher
 Exceptions thrown
UnificationException
ifinput
cannot be matched against the patternshape
.

def
apply(e1: Term, e2: Term): Subst
apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
.apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
. Definition Classes
 BaseMatcher → Matcher
 Exceptions thrown
UnificationException
ifinput
cannot be matched against the patternshape
.

def
apply(e1: Expression, e2: Expression): Subst
apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
.apply(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
. Definition Classes
 BaseMatcher → Matcher → Function2

final
def
asInstanceOf[T0]: T0
 Definition Classes
 Any

def
clone(): AnyRef
 Attributes
 protected[java.lang]
 Definition Classes
 AnyRef
 Annotations
 @native() @throws( ... )

def
coloredDotsTerm(s: Sort, color: Int = 0): Term
DotTerms of different "colors" for components of a Tuple, uncolored DotTerm for nonTuples
DotTerms of different "colors" for components of a Tuple, uncolored DotTerm for nonTuples
 Definition Classes
 SchematicUnificationMatch
coloredDotsTerm(Real) = • coloredDotsTerm(Real*Real) = (•_0, •_1) coloredDotsTerm(Real*Real*Real) = (•_0, •_1, •_2)
Example: 
def
compose(after: List[SubstRepl], before: List[SubstRepl]): List[SubstRepl]
Quickly compose patterns coming from fresh shapes by just concatenating them.
Quickly compose patterns coming from fresh shapes by just concatenating them. If indeed the shape used fresh names that did not occur in the input, this fast composition is fine.
 returns
a substitution that has the same effect as applying substitution
after
after applying substitutionbefore
.
 Attributes
 protected
 Definition Classes
 FreshUnificationMatch → SchematicUnificationMatch

def
curried: (Expression) ⇒ (Expression) ⇒ RenUSubst
 Definition Classes
 Function2
 Annotations
 @unspecialized()

def
distinctIfNeedBe(repl: List[SubstRepl]): List[SubstRepl]
Make
repl
distinct fast by directly returning it since this algorithm preserves distinctness in compose.Make
repl
distinct fast by directly returning it since this algorithm preserves distinctness in compose. returns
repl.distinct
 Attributes
 protected
 Definition Classes
 FreshUnificationMatch → SchematicComposedUnificationMatch

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

val
id: List[SubstRepl]
Identity substitution
{}
that does not change anything.Identity substitution
{}
that does not change anything. Attributes
 protected
 Definition Classes
 Matcher

final
def
isInstanceOf[T0]: Boolean
 Definition Classes
 Any

def
join(s: List[SubstRepl], t: List[SubstRepl]): List[SubstRepl]
Union of renaming substitution representations:
join(s, t)
gives the representation ofs
performed together witht
, if compatible.Union of renaming substitution representations:
join(s, t)
gives the representation ofs
performed together witht
, if compatible.s \cup t = {p(.)~>F  (p(.)~>F) \in s} ++ {(p(.)~>F)  (p(.)~>F) \in t} if s and t are compatible, so do not map the same p(.) or f(.) or a to different replacements
 returns
a substitution that has the same effect as applying both substitutions
s
andt
simultaneously. Similar to returnings++t
but skipping duplicates and checking compatibility in passing.
 Attributes
 protected
 Definition Classes
 BaseMatcher

lazy val
logger: Logger
 Attributes
 protected
 Definition Classes
 LazyLogging → LoggerHolder

final
val
loggerName: String
 Attributes
 protected
 Definition Classes
 LoggerHolder

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
 Function2 → AnyRef → Any

def
tupled: ((Expression, Expression)) ⇒ RenUSubst
 Definition Classes
 Function2
 Annotations
 @unspecialized()

def
unifiable(shape: Sequent, input: Sequent): Option[Subst]
unifiable(shape, input) Compute some unifier matching
input
against the patternshape
if unifiable else Noneunifiable(shape, input) Compute some unifier matching
input
against the patternshape
if unifiable else None Definition Classes
 BaseMatcher → Matcher

def
unifiable(shape: Expression, input: Expression): Option[Subst]
unifiable(shape, input) Compute some unifier matching
input
against the patternshape
if unifiable else Noneunifiable(shape, input) Compute some unifier matching
input
against the patternshape
if unifiable else None Definition Classes
 BaseMatcher → Matcher

def
unifier(e1: Expression, e2: Expression, us: List[SubstRepl]): Subst
Create the unifier
us
(which was formed for e1 and e2, just for the record).Create the unifier
us
(which was formed for e1 and e2, just for the record). Attributes
 protected
 Definition Classes
 FreshUnificationMatch → BaseMatcher

def
unifier(e1: Sequent, e2: Sequent, us: List[SubstRepl]): Subst
Create the unifier
us
(which was formed for e1 and e2, just for the record).Create the unifier
us
(which was formed for e1 and e2, just for the record). Attributes
 protected
 Definition Classes
 BaseMatcher

def
unifier(shape: Expression, input: Expression): List[SubstRepl]
Construct the base unifier that forces
shape
andinput
to unify unless equal alreadyConstruct the base unifier that forces
shape
andinput
to unify unless equal already returns
{shape~>input} unless shape=input in which case it's {}.
 Attributes
 protected
 Definition Classes
 BaseMatcher

def
unifies2(s1: Program, s2: Program, t1: Program, t2: Program): List[SubstRepl]
 Attributes
 protected
 Definition Classes
 SchematicComposedUnificationMatch → SchematicUnificationMatch

def
unifies2(s1: Formula, s2: Formula, t1: Formula, t2: Formula): List[SubstRepl]
 Attributes
 protected
 Definition Classes
 SchematicComposedUnificationMatch → SchematicUnificationMatch

def
unifies2(s1: Term, s2: Term, t1: Term, t2: Term): List[SubstRepl]
 Attributes
 protected
 Definition Classes
 SchematicComposedUnificationMatch → SchematicUnificationMatch

def
unifies2(s1: Expression, s2: Expression, t1: Expression, t2: Expression): List[SubstRepl]
unifies2(s1,s2, t1,t2)
unifies the two expressions of shape (s2,s2) against the two inputs (t1,t2) by singlesided matching.unifies2(s1,s2, t1,t2)
unifies the two expressions of shape (s2,s2) against the two inputs (t1,t2) by singlesided matching.s1 = t1  u1 u1(s2) = t2  u2  (s1,s2) = (t1,t2)  u2 after u1
Implemented by unifying from left to right, but will fall back to converse direction if exception.
 Attributes
 protected
 Definition Classes
 SchematicComposedUnificationMatch → SchematicUnificationMatch

def
unifiesODE2(s1: DifferentialProgram, s2: DifferentialProgram, t1: DifferentialProgram, t2: DifferentialProgram): List[SubstRepl]
 Attributes
 protected
 Definition Classes
 SchematicComposedUnificationMatch → SchematicUnificationMatch

def
unify(s1: Sequent, s2: Sequent): List[SubstRepl]
unify(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
.unify(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
. Attributes
 protected
 Definition Classes
 SchematicComposedUnificationMatch → BaseMatcher
 Exceptions thrown
UnificationException
ifinput
cannot be matched against the patternshape
.

def
unify(e1: Program, e2: Program): List[SubstRepl]
A simple recursive unification algorithm for singlesided matching.
A simple recursive unification algorithm for singlesided matching. unify(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
. Attributes
 protected
 Definition Classes
 SchematicUnificationMatch → BaseMatcher

def
unify(e1: Formula, e2: Formula): List[SubstRepl]
A simple recursive unification algorithm for singlesided matching.
A simple recursive unification algorithm for singlesided matching. unify(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
. Attributes
 protected
 Definition Classes
 SchematicUnificationMatch → BaseMatcher

def
unify(e1: Term, e2: Term): List[SubstRepl]
A simple recursive unification algorithm for singlesided matching.
A simple recursive unification algorithm for singlesided matching. unify(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
. Attributes
 protected
 Definition Classes
 SchematicUnificationMatch → BaseMatcher

def
unify(shape: Expression, input: Expression): List[SubstRepl]
 Attributes
 protected
 Definition Classes
 BaseMatcher

def
unifyApplicationOf(F: (Function, Term) ⇒ Expression, f: Function, t: Term, e2: Expression): List[SubstRepl]
Unify
f(t)
withe2
whereF
is the operator (FuncOf
orPredOf
) that forms the ApplicationOff(t)
.Unify
f(t)
withe2
whereF
is the operator (FuncOf
orPredOf
) that forms the ApplicationOff(t)
.1) unify the argument
t
with a DotTerm abstraction•
(t may be a tuple, then•
is a tuple: coloredDotsTerm)ua = unify(•, t)
2) unifier = substitute with the inverse of the argument unifier e2f(•) ~> ua^1(e2)
 Attributes
 protected
 Definition Classes
 SchematicUnificationMatch
given
t = (a, b)
,e2 = a^{2*b 1) unify((•_0, •_1), (a, b)) yields ua = •_0 ~> a, •_1 ~> b 2) the inverse is ua}1 = a ~> •_0, b ~> •_1
, thereforeua^{1(e2) = •_0}2*•_1
, resulting inf(•_0, •_1) ~> (•_0^2*•_1)
the inverse substitution is applied topdown, i.e., larger abstractions get precedence when components of
toverlap:
t = (x, y, x + y)and
e2 = x + yyields
f(•_0, •_1, •_2) ~> •_2; not
f(•_0, •_1, •_2) ~> •_0 + •_1
Example: 
def
unifyODE(e1: DifferentialProgram, e2: DifferentialProgram): List[SubstRepl]
A simple recursive unification algorithm for singlesided matching.
A simple recursive unification algorithm for singlesided matching. unify(shape, input) matches
input
against the patternshape
to find a uniform substitution\result
such that\result(shape)==input
. Attributes
 protected
 Definition Classes
 SchematicUnificationMatch → BaseMatcher

def
unifyVar(xp1: DifferentialSymbol, e2: Expression): List[SubstRepl]
unifyVar(x1',e2) gives a unifier making x1' equal to e2 unless it already is.
unifyVar(x1',e2) gives a unifier making x1' equal to e2 unless it already is.
 returns
unifyVar(x1',x2')={x1~>x2} if x2' is a differential variable other than x1' unifyVar(x1',x1')={}
 Attributes
 protected
 Definition Classes
 SchematicUnificationMatch
 Exceptions thrown
UnificationException
if e2 is not a differential variable

def
unifyVar(x1: Variable, e2: Expression): List[SubstRepl]
unifyVar(x1,e2) gives a unifier making x1 equal to e2 unless it already is.
unifyVar(x1,e2) gives a unifier making x1 equal to e2 unless it already is.
 returns
unifyVar(x1,x2)={x1~>x2} if x2 is a variable other than x1. unifyVar(x1,x1)={}
 Attributes
 protected
 Definition Classes
 SchematicUnificationMatch
 Exceptions thrown
UnificationException
if e2 is not a variable

def
ununifiable(shape: Sequent, input: Sequent): Nothing
Indicates that
input
cannot be matched against the patternshape
by raising a UnificationException.Indicates that
input
cannot be matched against the patternshape
by raising a UnificationException. Attributes
 protected
 Definition Classes
 BaseMatcher
 Exceptions thrown
UnificationException
always.

def
ununifiable(shape: Expression, input: Expression): Nothing
Indicates that
input
cannot be matched against the patternshape
by raising a UnificationException.Indicates that
input
cannot be matched against the patternshape
by raising a UnificationException. Attributes
 protected
 Definition Classes
 BaseMatcher
 Exceptions thrown
UnificationException
always.

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