trait HilbertCalculus extends UnifyUSCalculus
Hilbert Calculus for differential dynamic logic.
Provides the axioms and axiomatic proof rules from Figure 2 and Figure 3 in: Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 2016.
 See also
edu.cmu.cs.ls.keymaerax.core.AxiomBase
HilbertCalculus.derive()
HilbertCalculus.stepAt()
Andre Platzer. The complete proof theory of hybrid systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 541550. IEEE 2012
Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 1324. IEEE 2012
Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980
Andre Platzer. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.
Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
 Alphabetic
 By Inheritance
 HilbertCalculus
 UnifyUSCalculus
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Type Members

type
ForwardPositionTactic = (Position) ⇒ ForwardTactic
Forwardstyle position tactic mapping positions and provables to provables that follow from it.
Forwardstyle position tactic mapping positions and provables to provables that follow from it.
 Definition Classes
 UnifyUSCalculus

type
ForwardTactic = (ProvableSig) ⇒ ProvableSig
Forwardstyle tactic mapping provables to provables that follow from it.
Forwardstyle tactic mapping provables to provables that follow from it.
 Definition Classes
 UnifyUSCalculus

type
Subst = RenUSubst
The (generalized) substitutions used for unification
The (generalized) substitutions used for unification
 Definition Classes
 UnifyUSCalculus
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
CE(C: Context[Formula]): ForwardTactic
CE(C) will wrap any equivalence
left<>right
or equalityleft=right
fact it gets within context C.CE(C) will wrap any equivalence
left<>right
or equalityleft=right
fact it gets within context C. Uses CE or CQ as needed.p(x) <> q(x)  CE C{p(x)} <> C{q(x)}
f(x) = g(x)  CQ+CE c(f(x)) <> c(g(x))
 Definition Classes
 UnifyUSCalculus
 To do
likewise for Context[Term] using CT instead.
 See also
CMon(Context)
CEat(Provable)
CE(PosInExpr

def
CE(inEqPos: PosInExpr): DependentTactic
CE(pos) at the indicated position within an equivalence reduces contextual equivalence
C{left}<>C{right}
to argument equivalenceleft<>right
.CE(pos) at the indicated position within an equivalence reduces contextual equivalence
C{left}<>C{right}
to argument equivalenceleft<>right
.p(x) <> q(x)  CE C{p(x)} <> C{q(x)}
Part of the differential dynamic logic Hilbert calculus.
 inEqPos
the position *within* the two sides of the equivalence at which the context DotFormula occurs.
 Definition Classes
 UnifyUSCalculus
 See also
Andre Platzer. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.
Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.
UnifyUSCalculus.CEat(Provable)
UnifyUSCalculus.CMon(PosInExpr)
UnifyUSCalculus.CQ(PosInExpr)
UnifyUSCalculus.CE(Context)

def
CEat(fact: ProvableSig, C: Context[Formula]): DependentPositionTactic
CEat(fact,C) uses the equivalence
left<>right
or equalityleft=right
or implicationleft>right
fact for congruence reasoning in the given context C at the indicated position to replaceright
byleft
in that context (literally, no substitution).CEat(fact,C) uses the equivalence
left<>right
or equalityleft=right
or implicationleft>right
fact for congruence reasoning in the given context C at the indicated position to replaceright
byleft
in that context (literally, no substitution). Definition Classes
 UnifyUSCalculus
CE(fact, Context("x>0&⎵".asFormula))(p)
is equivalent toCE(fact)(p+PosInExpr(1::Nil))
. Except that the former has the shapex>0&⎵
for the context starting from positionp
. , CE(fact, Context("⎵".asFormula))
is equivalent toCE(fact)
. See also
UnifyUSCalculus.CMon(PosInExpr)
UnifyUSCalculus.CQ(PosInExpr)
UnifyUSCalculus.CE(PosInExpr)
CE(Context)
useAt()
UnifyUSCalculus.CEat(Provable)
Examples: 
def
CEat(fact: ProvableSig): DependentPositionTactic
CEat(fact) uses the equivalence
left<>right
or equalityleft=right
or implicationleft>right
fact for congruence reasoning at the indicated position to replaceright
byleft
at indicated position (literally, no substitution).CEat(fact) uses the equivalence
left<>right
or equalityleft=right
or implicationleft>right
fact for congruence reasoning at the indicated position to replaceright
byleft
at indicated position (literally, no substitution). Efficient unificationfree version of PosInExpr):PositionTacticfact G  C{q(x)}, D q(x) <> p(x)  CER(fact) G  C{p(x)}, D
Similarly for antecedents or equality facts or implication facts, e.g.:
fact C{q(x)}, G  D q(x) <> p(x)  CEL(fact) C{p(x)}, G  D
 Definition Classes
 UnifyUSCalculus
CEat(fact)
is equivalent toCEat(fact, Context("⎵".asFormula))
 To do
Optimization: Would direct propositional rules make CEat faster at pos.isTopLevel?
 See also
UnifyUSCalculus.CMon(PosInExpr)
UnifyUSCalculus.CQ(PosInExpr)
UnifyUSCalculus.CE(PosInExpr)
CE(Context)
useAt()
UnifyUSCalculus.CEat(Provable,Context)
Example: 
def
CMon(C: Context[Formula]): ForwardTactic
CMon(C) will wrap any implication
left>right
fact it gets within a (positive or negative) context C by monotonicity.CMon(C) will wrap any implication
left>right
fact it gets within a (positive or negative) context C by monotonicity.k  o  CMon if C{⎵} of positive polarity C{k}  C{o}
 Definition Classes
 UnifyUSCalculus
 Note
The direction in the conclusion switches for negative polarity C{⎵}
 See also
CE(Context)
UnifyUSCalculus.CMon(PosInExpr)

def
CMon: DependentPositionTactic
Convenience CMon with hiding.
Convenience CMon with hiding.
 Definition Classes
 UnifyUSCalculus

def
CMon(inEqPos: PosInExpr): DependentTactic
CMon(pos) at the indicated position within an implication reduces contextual implication
C{o}>C{k}
to argument implicationo>k
for positive C.CMon(pos) at the indicated position within an implication reduces contextual implication
C{o}>C{k}
to argument implicationo>k
for positive C. o > k  for positive C{.}  C{o} > C{k}
 inEqPos
the position *within* the two sides of the implication at which the context DotFormula happens.
 Definition Classes
 UnifyUSCalculus
 See also
UnifyUSCalculus.CEat())
UnifyUSCalculus.CMon(Context)
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CQ(PosInExpr)

def
CQ(inEqPos: PosInExpr): DependentTactic
CQ(pos) at the indicated position within an equivalence reduces contextual equivalence
p(left)<>p(right)
to argument equalityleft=right
.CQ(pos) at the indicated position within an equivalence reduces contextual equivalence
p(left)<>p(right)
to argument equalityleft=right
. This tactic will use CEat() under the hood as needed.f(x) = g(x)  CQ c(f(x)) <> c(g(x))
 inEqPos
the position *within* the two sides of the equivalence at which the context DotTerm happens.
 Definition Classes
 UnifyUSCalculus
 See also
UnifyUSCalculus.CMon(PosInExpr)
UnifyUSCalculus.CE(PosInExpr)

def
DC(invariant: Formula): DependentPositionTactic
DC: Differential Cut a new invariant for a differential equation
[{x'=f(x)&q(x)}]p(x)
reduces to[{x'=f(x)&q(x)&C(x)}]p(x)
with[{x'=f(x)&q(x)}]C(x)
. 
def
DCd(invariant: Formula): DependentPositionTactic
DCd: Diamond Differential Cut a new invariant for a differential equation
<{x'=f(x)&q(x)}>p(x)
reduces to<{x'=f(x)&q(x)&C(x)}>p(x)
with[{x'=f(x)&q(x)}]C(x)
. 
lazy val
DE: DependentPositionTactic
DE: Differential Effect exposes the effect of a differential equation
[x'=f(x)]p(x,x')
on its differential symbols as[x'=f(x)][x':=f(x)]p(x,x')
with its differential assignmentx':=f(x)
.DE: Differential Effect exposes the effect of a differential equation
[x'=f(x)]p(x,x')
on its differential symbols as[x'=f(x)][x':=f(x)]p(x,x')
with its differential assignmentx':=f(x)
.G  [{x'=f()&H()}][x':=f();]p(), D  G  [{x'=f()&H()}]p(), D
 [{x'=1, y'=x & x>0}][y':=x;][x':=1;]x>0 DE(1)  [{x'=1, y'=x & x>0}]x>0
,  [{x'=1}][x':=1;]x>0 DE(1)  [{x'=1}]x>0
Examples: 
lazy val
DI: DependentPositionTactic
DI: Differential Invariants are used for proving a formula to be an invariant of a differential equation.
DI: Differential Invariants are used for proving a formula to be an invariant of a differential equation.
[x'=f(x)&q(x)]p(x)
reduces toq(x) > p(x) & [x'=f(x)]p(x)'
. See also
DifferentialTactics.diffInd()

lazy val
DS: DependentPositionTactic
DS: Differential Solution solves a simple differential equation
[x'=c&q(x)]p(x)
by reduction to\forall t>=0 ((\forall 0<=s<=t q(x+c()*s) > [x:=x+c()*t;]p(x))

lazy val
DW: DependentPositionTactic
DW: Differential Weakening to use evolution domain constraint
[{x'=f(x)&q(x)}]p(x)
reduces to[{x'=f(x)&q(x)}](q(x)>p(x))

lazy val
DWd: DependentPositionTactic
DWd: Diamond Differential Weakening to use evolution domain constraint
<{x'=f(x)&q(x)}>p(x)
reduces to<{x'=f(x)&q(x)}>(q(x)&p(x))

lazy val
Dassignb: DependentPositionTactic
Dassignb: [':=] Substitute a differential assignment
[x':=f]p(x')
top(f)

val
G: DependentPositionTactic
G: Gödel generalization rule reduces a proof of
 [a]p(x)
to proving the postcondition p(x)
in isolation. 
lazy val
K: DependentPositionTactic
K: modal modus ponens (hybrid systems)

def
US(fact: ProvableSig): DependentTactic
US(fact) uses a suitable uniform substitution to reduce the proof to the proof of
fact
.US(fact) uses a suitable uniform substitution to reduce the proof to the proof of
fact
. Unifies the current sequent withfact.conclusion
. Use that unifier as a uniform substitution to instantiatefact
with.fact: g  d  US where G=s(g) and D=s(d) where s=unify(fact.conclusion, GD) G  D
 fact
the proof to reduce this proof to by a suitable Uniform Substitution.
 Definition Classes
 UnifyUSCalculus
 See also
byUS()

def
US(subst: USubst): BuiltInTactic
 Definition Classes
 UnifyUSCalculus

def
US(subst: USubst, axiom: String): BuiltInTactic
US(subst, axiom) reduces the proof to the given axiom, whose uniform substitution instance under
subst
the current goal is.US(subst, axiom) reduces the proof to the given axiom, whose uniform substitution instance under
subst
the current goal is. Definition Classes
 UnifyUSCalculus

def
US(subst: USubst, fact: ProvableSig): BuiltInTactic
US(subst, fact) reduces the proof to a proof of
fact
, whose uniform substitution instance undersubst
the current goal is.US(subst, fact) reduces the proof to a proof of
fact
, whose uniform substitution instance undersubst
the current goal is. Definition Classes
 UnifyUSCalculus
 See also
edu.cmu.cs.ls.keymaerax.core.Provable.apply(USubst)

lazy val
V: DependentPositionTactic
V: vacuous box
[a]p()
will be discarded and replaced byp()
provided programa
does not change values of postconditionp()
.V: vacuous box
[a]p()
will be discarded and replaced byp()
provided programa
does not change values of postconditionp()
. Note
Unsound for hybrid games

lazy val
VK: DependentPositionTactic
VK: vacuous box
[a]p()
will be discarded and replaced byp()
provided programa
does not change values of postconditionp()
and provided[a]true
proves, e.g., sincea
is a hybrid system.  lazy val allDist: DependentPositionTactic

lazy val
allG: BelleExpr
allG: all generalization rule reduces a proof of
 \forall x p(x)
to proving p(x)
in isolation 
lazy val
allV: DependentPositionTactic
allV: vacuous
\forall x p()
will be discarded and replaced by p() provided x does not occur in p(). 
final
def
asInstanceOf[T0]: T0
 Definition Classes
 Any

lazy val
assignb: DependentPositionTactic
assignb: [:=] simplify assignment
[x:=f;]p(x)
by substitutionp(f)
or equation.assignb: [:=] simplify assignment
[x:=f;]p(x)
by substitutionp(f)
or equation. Box assignment by substitution assignment [v:=t();]p(v) <> p(t()) (preferred), or by equality assignment [x:=f();]p() <> \forall x (x=f() > p()) as a fallback. Universal quantifiers are skolemized if applied at toplevel in the succedent; they remain unhandled in the antecedent and in nontoplevel context. [y:=2;]\\forall x_0 (x_0=1 > x_0=1 > [{x_0:=x_0+1;}*]x_0>0) assignb(1, 1::Nil)  [y:=2;][x:=1;][{x:=x+1;}*]x>0
, \\forall x_0 (x_0=1 > [{x_0:=x_0+1;}*]x_0>0)  assignb(1) [x:=1;][{x:=x+1;}*]x>0 
, x_0=1  [{x_0:=x_0+1;}*]x_0>0 assignb(1)  [x:=1;][{x:=x+1;}*]x>0
, 1>0  assignb(1) [x:=1;]x>0 
,  1>0 assignb(1)  [x:=1;]x>0
 See also
DLBySubst.assignEquality
Examples: 
lazy val
assignd: DependentPositionTactic
assignd: <:=> simplify assignment
<x:=f;>p(x)
by substitutionp(f)
or equation 
def
boundRename(what: Variable, repl: Variable): DependentPositionTactic
boundRename(what,repl) renames
what
torepl
at the indicated position (or vice versa).boundRename(what,repl) renames
what
torepl
at the indicated position (or vice versa). Definition Classes
 UnifyUSCalculus
 See also

lazy val
box: DependentPositionTactic
box: [.] to reduce doublenegated diamond
!⟨a⟩!p(x)
to a box[a]p(x)
. 
lazy val
boxAnd: DependentPositionTactic
boxAnd: splits
[a](p&q)
into[a]p & [a]q

lazy val
boxImpliesAnd: DependentPositionTactic
boxImpliesAnd: splits
[a](p>q&r)
into[a](p>q) & [a](p>r)

val
boxTrue: DependentPositionTactic
boxTrue: proves
[a]true
directly for hybrid systemsa
that are not hybrid games. 
def
by(name: String, subst: Subst): BelleExpr
by(name,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.
by(name,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.
 Definition Classes
 UnifyUSCalculus

def
by(name: String, subst: USubst): BelleExpr
by(name,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.
by(name,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.
s(a)  s(b) a  b  rule() if s(g)=G and s(d)=D G  D g  d
 name
the name of the fact to use to prove the sequent
 subst
what substitution
s
to use for instantiating the fact calledname
.
 Definition Classes
 UnifyUSCalculus
 See also
byUS()

def
by(lemma: Lemma, name: String): BelleExpr
 Definition Classes
 UnifyUSCalculus

def
by(lemma: Lemma): BelleExpr
by(lemma) uses the given Lemma literally to continue or close the proof (if it fits to what has been proved)
by(lemma) uses the given Lemma literally to continue or close the proof (if it fits to what has been proved)
 Definition Classes
 UnifyUSCalculus

def
by(fact: ProvableSig, name: String = "by"): BuiltInTactic
by(provable) uses the given Provable literally to continue or close the proof (if it fits to what has been proved so far)
by(provable) uses the given Provable literally to continue or close the proof (if it fits to what has been proved so far)
 Definition Classes
 UnifyUSCalculus

def
byUS(name: String, inst: (Subst) ⇒ Subst = us=>us): BelleExpr
rule(name,inst) uses the given axiomatic rule to prove the sequent.
rule(name,inst) uses the given axiomatic rule to prove the sequent. Unifies the fact's conclusion with the current sequent and proceed to the instantiated premise of
fact
.s(a)  s(b) a  b  rule() if s(g)=G and s(d)=D G  D g  d
The behavior of rule(Provable) is essentially the same as that of by(Provable) except that the former prefetches the uniform substitution instance during tactics applicability checking.
 name
the name of the fact to use to prove the sequent
 inst
Transformation for instantiating additional unmatched symbols that do not occur in the conclusion. Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the mostgeneral unifier are preferred.
 Definition Classes
 UnifyUSCalculus
 See also
by()
byUS()

def
byUS(name: String): BelleExpr
byUS(axiom) proves by a uniform substitution instance of a (derived) axiom or (derived) axiomatic rule.
byUS(axiom) proves by a uniform substitution instance of a (derived) axiom or (derived) axiomatic rule.
 Definition Classes
 UnifyUSCalculus
 See also
UnifyUSCalculus.byUS()

def
byUS(lemma: Lemma): BelleExpr
byUS(lemma) proves by a uniform substitution instance of lemma.
byUS(lemma) proves by a uniform substitution instance of lemma.
 Definition Classes
 UnifyUSCalculus

def
byUS(provable: ProvableSig): BelleExpr
byUS(provable) proves by a uniform substitution instance of provable, obtained by unification with the current goal.
byUS(provable) proves by a uniform substitution instance of provable, obtained by unification with the current goal.
 Definition Classes
 UnifyUSCalculus
 See also
UnifyUSCalculus.US()

def
chase(keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst = ax=>us=>us, index: (String) ⇒ (PosInExpr, List[PosInExpr]) = AxiomIndex.axiomIndex): DependentPositionTactic
chase: Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices.
chase: Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices.
Chase the expression at the indicated position forward (Hilbert computation constructing the answer by proof). Follows canonical axioms toward all their recursors while there is an applicable simplifier axiom according to
keys
. keys
maps expressions to a list of axiom names to be used for those expressions. First returned axioms will be favored (if applicable) over further axioms.
 modifier
will be notified after successful uses of axiom at a position with the result of the use. The result of modifier(ax,pos)(step) will be used instead of step for each step of the chase.
 inst
Transformation for instantiating additional unmatched symbols that do not occur when using the given axiom _1. Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the mostgeneral unifier are preferred.
 index
Provides recursors to continue chase after applying an axiom from
keys
. Defaults to AxiomIndex.axiomIndex.
 Definition Classes
 UnifyUSCalculus
When applied at 1::Nil, turns [{x'=22}][?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into [{x'=22}]((x>0>x+1>=1) & (x=0>1>=1))
, When applied at Nil, turns [?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into ((x>0>x+1>=1) & (x=0>1>=1))
, When applied at 1::Nil, turns [{x'=22}](2*x+x*y>=5)' into [{x'=22}]2*x'+(x'*y+x*y')>=0
 To do
also implement a backwards chase in tableaux/sequent style based on useAt instead of useFor
 Note
Chase is searchfree and, thus, quite efficient. It directly follows the axiom index information to compute followup positions for the chase.
 See also
chaseFor()
Examples: 
def
chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

def
chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String]): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

def
chase(breadth: Int, giveUp: Int): DependentPositionTactic
Chase with bounded breadth and giveUp to stop.
Chase with bounded breadth and giveUp to stop.
 breadth
how many alternative axioms to pursue locally, using the first applicable one. Equivalent to pruning keys so that all lists longer than giveUp are replaced by Nil, and then all lists are truncated beyond breadth.
 giveUp
how many alternatives are too much so that the chase stops without trying any for applicability. Equivalent to pruning keys so that all lists longer than giveUp are replaced by Nil.
 Definition Classes
 UnifyUSCalculus

lazy val
chase: DependentPositionTactic
Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices.
Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices. Unlike TactixLibrary.tacticChase will not branch or use propositional rules, merely transform the chosen formula in place.
 Definition Classes
 UnifyUSCalculus

def
chaseCustom(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): DependentPositionTactic
chaseCustom: Unrestricted form of chaseFor, where AxiomIndex is not built in, i.e.
chaseCustom: Unrestricted form of chaseFor, where AxiomIndex is not built in, i.e. it takes keys of the form Expression => List[(Provable,PosInExpr, List[PosInExpr])] This allows customised rewriting
 Definition Classes
 UnifyUSCalculus

def
chaseCustomFor(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): ForwardPositionTactic
 Definition Classes
 UnifyUSCalculus

def
chaseFor(keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst = ax=>us=>us, index: (String) ⇒ (PosInExpr, List[PosInExpr])): ForwardPositionTactic
chaseFor: Chases the expression of Provables at given positions forward until it is chased away or can't be chased further without critical choices.
chaseFor: Chases the expression of Provables at given positions forward until it is chased away or can't be chased further without critical choices.
Chase the expression at the indicated position forward (Hilbert computation constructing the answer by proof). Follows canonical axioms toward all their recursors while there is an applicable simplifier axiom according to
keys
. keys
maps expressions to a list of axiom names to be used for those expressions. First returned axioms will be favored (if applicable) over further axioms.
 modifier
will be notified after successful uses of axiom at a position with the result of the use. The result of modifier(ax,pos)(step) will be used instead of step for each step of the chase.
 inst
Transformation for instantiating additional unmatched symbols that do not occur when using the given axiom _1. Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the mostgeneral unifier are preferred.
 Definition Classes
 UnifyUSCalculus
When applied at 1::Nil, turns [{x'=22}][?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into [{x'=22}]((x>0>x+1>=1) & (x=0>1>=1))
, When applied at Nil, turns [?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into ((x>0>x+1>=1) & (x=0>1>=1))
, When applied at 1::Nil, turns [{x'=22}](2*x+x*y>=5)' into [{x'=22}]2*x'+(x'*y+x*y')>=0
 Note
Chase is searchfree and, thus, quite efficient. It directly follows the axiom index information to compute followup positions for the chase.
 See also
UnifyUSCalculus.useFor()
chase()
Examples: 
def
chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst, index: (String) ⇒ (PosInExpr, List[PosInExpr])): ForwardPositionTactic
 Definition Classes
 UnifyUSCalculus

def
chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst): ForwardPositionTactic
 Definition Classes
 UnifyUSCalculus

def
chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic): ForwardPositionTactic
 Definition Classes
 UnifyUSCalculus

def
chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst, index: (String) ⇒ (PosInExpr, List[PosInExpr])): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

def
chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

def
chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], inst: (String) ⇒ (Subst) ⇒ Subst): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

lazy val
choiceb: DependentPositionTactic
choiceb: [++] handles both cases of a nondeterministic choice
[a++b]p(x)
separately[a]p(x) & [b]p(x)

lazy val
choiced: DependentPositionTactic
choiced: <++> handles both cases of a nondeterministic choice
⟨a++b⟩p(x)
separately⟨a⟩p(x)  ⟨b⟩p(x)

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

def
commuteEquivFR: ForwardPositionTactic
commuteEquivFR commutes the equivalence at the given position (for forward tactics).
commuteEquivFR commutes the equivalence at the given position (for forward tactics).
 Definition Classes
 UnifyUSCalculus

lazy val
composeb: DependentPositionTactic
composeb: [;] handle both parts of a sequential composition
[a;b]p(x)
one at a time[a][b]p(x)

lazy val
composed: DependentPositionTactic
composed: <;> handle both parts of a sequential composition
⟨a;b⟩p(x)
one at a time⟨a⟩⟨b⟩p(x)

def
cutAt(repl: Expression): DependentPositionTactic
cutAt(repl) cuts left/right to replace the expression at the indicated position in its context C{.} by
repl
.cutAt(repl) cuts left/right to replace the expression at the indicated position in its context C{.} by
repl
.G  C{repl}, D G  C{repl}>C{c}, D  cutAt(repl) G  C{c}, D
C{repl}, G  D G  D, C{c}>C{repl}  cutAt(repl) C{c}, G  D
 Definition Classes
 UnifyUSCalculus
 See also
UnifyUSCalculus.CEat(Provable)

lazy val
derive: DependentPositionTactic
Derive the differential expression at the indicated position (Hilbert computation deriving the answer by proof).
Derive the differential expression at the indicated position (Hilbert computation deriving the answer by proof).
When applied at 1::Nil, turns [{x'=22}](2*x+x*y>=5)' into [{x'=22}]2*x'+x'*y+x*y'>=0
 See also
Example: 
lazy val
diamond: DependentPositionTactic
diamond: <.> reduce doublenegated box
![a]!p(x)
to a diamond⟨a⟩p(x)
. 
lazy val
diamondOr: DependentPositionTactic
diamondOr: splits
⟨a⟩(pq)
into⟨a⟩p  ⟨a⟩q

lazy val
dualb: DependentPositionTactic
dualb: [^{d}] handle dual game
[{a}^{d}]p(x)
by![a]!p(x)

lazy val
duald: DependentPositionTactic
duald:
<^{d}>
handle dual game⟨{a}^{d}⟩p(x)
by!⟨a⟩!p(x)

def
either(left: ForwardTactic, right: ForwardTactic): ForwardTactic
either(left,right) runs
left
if successful andright
otherwise (for forward tactics).either(left,right) runs
left
if successful andright
otherwise (for forward tactics). Definition Classes
 UnifyUSCalculus

def
eitherP(left: ForwardPositionTactic, right: ForwardPositionTactic): ForwardPositionTactic
eitherP(left,right) runs
left
if successful andright
otherwise (for forward tactics).eitherP(left,right) runs
left
if successful andright
otherwise (for forward tactics). Definition Classes
 UnifyUSCalculus

final
def
eq(arg0: AnyRef): Boolean
 Definition Classes
 AnyRef

def
equals(arg0: Any): Boolean
 Definition Classes
 AnyRef → Any
 lazy val existsE: DependentPositionTactic

lazy val
existsV: DependentPositionTactic
existsV: vacuous
\exists x p()
will be discarded and replaced by p() provided x does not occur in p(). 
def
finalize(): Unit
 Attributes
 protected[java.lang]
 Definition Classes
 AnyRef
 Annotations
 @throws( classOf[java.lang.Throwable] )

def
fromAxIndex(s: String): (ProvableSig, PosInExpr, List[PosInExpr])
 Definition Classes
 UnifyUSCalculus

final
def
getClass(): Class[_]
 Definition Classes
 AnyRef → Any
 Annotations
 @native()

def
hashCode(): Int
 Definition Classes
 AnyRef → Any
 Annotations
 @native()

def
iden: ForwardTactic
identity tactic skip that does not no anything (for forward tactics).
identity tactic skip that does not no anything (for forward tactics).
 Definition Classes
 UnifyUSCalculus

def
ifThenElse(cond: (ProvableSig) ⇒ Boolean, thenT: ForwardTactic, elseT: ForwardTactic): ForwardTactic
ifThenElse(cond,thenT,elseT) runs
thenT
ifcond
holds andelseT
otherwise (for forward tactics).ifThenElse(cond,thenT,elseT) runs
thenT
ifcond
holds andelseT
otherwise (for forward tactics). Definition Classes
 UnifyUSCalculus

def
ifThenElseP(cond: (Position) ⇒ (ProvableSig) ⇒ Boolean, thenT: ForwardPositionTactic, elseT: ForwardPositionTactic): ForwardPositionTactic
ifThenElseP(cond,thenT,elseT) runs
thenT
ifcond
holds andelseT
otherwise (for forward tactics).ifThenElseP(cond,thenT,elseT) runs
thenT
ifcond
holds andelseT
otherwise (for forward tactics). Definition Classes
 UnifyUSCalculus

final
def
isInstanceOf[T0]: Boolean
 Definition Classes
 Any

lazy val
iterateb: DependentPositionTactic
iterateb: [*] prove a property of a loop
[{a}*]p(x)
by unrolling it oncep(x) & [a][{a}*]p(x)

lazy val
iterated: DependentPositionTactic
iterated: <*> prove a property of a loop
⟨{a}*⟩p(x)
by unrolling it oncep(x)  ⟨a⟩⟨{a}*⟩p(x)

def
lazyUseAt(lemmaName: String, key: PosInExpr): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

def
lazyUseAt(lemmaName: String): DependentPositionTactic
Lazy useAt of a lemma by name.
Lazy useAt of a lemma by name. For use with ProveAs.
 Definition Classes
 UnifyUSCalculus

def
let(abbr: Expression, value: Expression, inner: BelleExpr): BelleExpr
Let(abbr, value, inner) alias
let abbr=value in inner
abbreviatesvalue
byabbr
in the provable and proceeds with an internal proof by tacticinner
, resuming to the outer proof by a uniform substitution ofvalue
forabbr
of the resulting provable.Let(abbr, value, inner) alias
let abbr=value in inner
abbreviatesvalue
byabbr
in the provable and proceeds with an internal proof by tacticinner
, resuming to the outer proof by a uniform substitution ofvalue
forabbr
of the resulting provable. Definition Classes
 UnifyUSCalculus

lazy val
monb: BelleExpr
monb: Monotone
[a]p(x)  [a]q(x)
reduces to provingp(x)  q(x)

lazy val
mond: BelleExpr
mond: Monotone
⟨a⟩p(x)  ⟨a⟩q(x)
reduces to provingp(x)  q(x)

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

lazy val
randomb: DependentPositionTactic
randomb: [:*] simplify nondeterministic assignment
[x:=*;]p(x)
to a universal quantifier\forall x p(x)

lazy val
randomd: DependentPositionTactic
randomd: <:*> simplify nondeterministic assignment
<x:=*;>p(x)
to an existential quantifier\exists x p(x)

def
seqCompose(first: ForwardTactic, second: ForwardTactic): ForwardTactic
seqCompose(first,second) runs
first
followed bysecond
(for forward tactics).seqCompose(first,second) runs
first
followed bysecond
(for forward tactics). Definition Classes
 UnifyUSCalculus

def
seqComposeP(first: ForwardPositionTactic, second: ForwardPositionTactic): ForwardPositionTactic
seqComposeP(first,second) runs
first
followed bysecond
(for forward tactics).seqComposeP(first,second) runs
first
followed bysecond
(for forward tactics). Definition Classes
 UnifyUSCalculus

def
stepAt(axiomIndex: (Expression) ⇒ Option[String]): DependentPositionTactic
Make the canonical simplifying proof step based at the indicated position except when an unknown decision needs to be made (e.g.
Make the canonical simplifying proof step based at the indicated position except when an unknown decision needs to be made (e.g. invariants for loops or for differential equations). Using the provided AxiomIndex.
 Definition Classes
 UnifyUSCalculus
 Note
Efficient sourcelevel indexing implementation.
 See also

val
stepAt: DependentPositionTactic
Make the canonical simplifying proof step at the indicated position except when a decision needs to be made (e.g.
Make the canonical simplifying proof step at the indicated position except when a decision needs to be made (e.g. invariants for loops or for differential equations). Using the canonical AxiomIndex.
 Note
Efficient sourcelevel indexing implementation.
 See also

final
def
synchronized[T0](arg0: ⇒ T0): T0
 Definition Classes
 AnyRef

lazy val
testb: DependentPositionTactic
testb: [?] simplifies test
[?q;]p
to an implicationq>p

lazy val
testd: DependentPositionTactic
testd: <?> simplifies test
<?q;>p
to a conjunctionq&p

def
toString(): String
 Definition Classes
 AnyRef → Any

def
uniformRename(ur: URename): InputTactic
uniformRename(ur) renames
ur.what
tour.repl
uniformly and vice versa.uniformRename(ur) renames
ur.what
tour.repl
uniformly and vice versa. Definition Classes
 UnifyUSCalculus
 See also

def
uniformRename(what: Variable, repl: Variable): InputTactic
uniformRename(what,repl) renames
what
torepl
uniformly and vice versa.uniformRename(what,repl) renames
what
torepl
uniformly and vice versa. Definition Classes
 UnifyUSCalculus
 See also

def
uniformRenameF(what: Variable, repl: Variable): ForwardTactic
uniformRenameF(what,repl) renames
what
torepl
uniformly (for forward tactics).uniformRenameF(what,repl) renames
what
torepl
uniformly (for forward tactics). Definition Classes
 UnifyUSCalculus

def
uniformSubstitute(subst: USubst): BuiltInTactic
 Definition Classes
 UnifyUSCalculus
 See also
US()

def
useAt(axiom: ProvableInfo, key: PosInExpr): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

def
useAt(axiom: ProvableInfo, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

def
useAt(axiom: String): DependentPositionTactic
useAt(axiom)(pos) uses the given (derived) axiom at the given position in the sequent (by unifying and equivalence rewriting).
useAt(axiom)(pos) uses the given (derived) axiom at the given position in the sequent (by unifying and equivalence rewriting).
 Definition Classes
 UnifyUSCalculus

def
useAt(axiom: String, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

def
useAt(axiom: String, key: PosInExpr): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

def
useAt(axiom: String, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
useAt(axiom)(pos) uses the given (derived) axiom at the given position in the sequent (by unifying and equivalence rewriting).
useAt(axiom)(pos) uses the given (derived) axiom at the given position in the sequent (by unifying and equivalence rewriting).
 key
the optional position of the key in the axiom to unify with. Defaults to AxiomIndex
 inst
optional transformation augmenting or replacing the uniform substitutions after unification with additional information.
 Definition Classes
 UnifyUSCalculus

def
useAt(lem: Lemma): DependentPositionTactic
useAt(lem)(pos) uses the given lemma at the given position in the sequent (by unifying and equivalence rewriting).
useAt(lem)(pos) uses the given lemma at the given position in the sequent (by unifying and equivalence rewriting).
 Definition Classes
 UnifyUSCalculus

def
useAt(lem: Lemma, key: PosInExpr): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

def
useAt(lem: Lemma, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
useAt(lem)(pos) uses the given lemma at the given position in the sequent (by unifying and equivalence rewriting).
useAt(lem)(pos) uses the given lemma at the given position in the sequent (by unifying and equivalence rewriting).
 key
the optional position of the key in the axiom to unify with. Defaults to AxiomIndex
 inst
optional transformation augmenting or replacing the uniform substitutions after unification with additional information.
 Definition Classes
 UnifyUSCalculus

def
useExpansionAt(axiom: String, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
 Definition Classes
 UnifyUSCalculus

def
useExpansionAt(axiom: String): DependentPositionTactic
useExpansionAt(axiom)(pos) uses the given axiom at the given position in the sequent (by unifying and equivalence rewriting) in the direction that expands as opposed to simplifies operators.
useExpansionAt(axiom)(pos) uses the given axiom at the given position in the sequent (by unifying and equivalence rewriting) in the direction that expands as opposed to simplifies operators.
 Definition Classes
 UnifyUSCalculus

def
useExpansionFor(axiom: String): ForwardPositionTactic
useExpansionFor(axiom) uses the given axiom forward to expand the given position in the sequent (by unifying and equivalence rewriting) in the direction that expands as opposed to simplifies operators.
useExpansionFor(axiom) uses the given axiom forward to expand the given position in the sequent (by unifying and equivalence rewriting) in the direction that expands as opposed to simplifies operators.
 Definition Classes
 UnifyUSCalculus

def
useFor(fact: ProvableSig, key: PosInExpr, inst: (Subst) ⇒ Subst = us => us): ForwardPositionTactic
useFor(fact,key,inst) use the key part of the given fact forward for the selected position in the given Provable to conclude a new Provable Forward Hilbertstyle proof analogue of useAt().
useFor(fact,key,inst) use the key part of the given fact forward for the selected position in the given Provable to conclude a new Provable Forward Hilbertstyle proof analogue of useAt().
G  C{c}, D  useFor(__l__<>r) if s=unify(c,l) G  C{s(r)}, D
and accordingly for facts that are
l>r
facts or conditionalp>(l<>r)
orp>(l>r)
facts and so on, wherel
indicates the key part of the fact. useAt automatically tries proving the required assumptions/conditions of the fact it is using.For facts of the form
prereq > (left<>right)
this tactic currently only uses master to prove
prereq
globally and otherwise gives up. fact
the Provable fact whose conclusion to use to simplify at the indicated position of the sequent
 key
the part of the fact's conclusion to unify the indicated position of the sequent with
 inst
Transformation for instantiating additional unmatched symbols that do not occur in
fact.conclusion(key)
. Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the mostgeneral unifier are preferred.
 Definition Classes
 UnifyUSCalculus
useFor(Axiom.axiom("[;] compose"), PosInExpr(0::Nil)) applied to the indicated 1::1::Nil of
turns it into[x:=1;][{x'=22}][x:=2*x;++x:=0;]x>=0
[x:=1;][{x'=22}] ([x:=2*x;]x>=0 & [x:=0;]x>=0)
 See also
useAt()
Example: 
def
useFor(axiom: String, key: PosInExpr, inst: (Subst) ⇒ Subst): ForwardPositionTactic
useFor(axiom, key) use the key part of the given axiom forward for the selected position in the given Provable to conclude a new Provable
useFor(axiom, key) use the key part of the given axiom forward for the selected position in the given Provable to conclude a new Provable
 key
the optional position of the key in the axiom to unify with. Defaults to AxiomIndex
 inst
optional transformation augmenting or replacing the uniform substitutions after unification with additional information.
 Definition Classes
 UnifyUSCalculus

def
useFor(axiom: String, key: PosInExpr): ForwardPositionTactic
useFor(axiom, key) use the key part of the given axiom forward for the selected position in the given Provable to conclude a new Provable
useFor(axiom, key) use the key part of the given axiom forward for the selected position in the given Provable to conclude a new Provable
 Definition Classes
 UnifyUSCalculus

def
useFor(axiom: String): ForwardPositionTactic
useFor(axiom) use the given axiom forward for the selected position in the given Provable to conclude a new Provable
useFor(axiom) use the given axiom forward for the selected position in the given Provable to conclude a new Provable
 Definition Classes
 UnifyUSCalculus

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

object
Derive
Derive: provides individual differential axioms bundled as HilbertCalculus.derive.
Derive: provides individual differential axioms bundled as HilbertCalculus.derive.
There is rarely a reason to use these separate axioms, since HilbertCalculus.derive already uses the appropriate differential axiom as needed.
 See also
Figure 3 in Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 2016.
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 structuresedu.cmu.cs.ls.keymaerax.core.Expression
 Differential dynamic logic expressionsedu.cmu.cs.ls.keymaerax.core.Sequent
 Sequents of formulasedu.cmu.cs.ls.keymaerax.core.Rule
 Proof rulesedu.cmu.cs.ls.keymaerax.core.Provable
 Proof certificateedu.cmu.cs.ls.keymaerax.btactics
 Tactic language libraryedu.cmu.cs.ls.keymaerax.btactics.TactixLibrary
 Main tactic libraryedu.cmu.cs.ls.keymaerax.btactics.HilbertCalculus
 Hilbert Calculus for differential dynamic logicedu.cmu.cs.ls.keymaerax.btactics.SequentCalculus
 Sequent Calculus for propositional and firstorder logicedu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus
 Unificationbased Uniform Substitution Calculusedu.cmu.cs.ls.keymaerax.bellerophon
 Bellerophon tactic language and tactic interpreteredu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr
 Tactic language expressionsedu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter
 Sequential tactic interpreteredu.cmu.cs.ls.keymaerax.parser
 Parser and pretty printer with concrete syntax and notation for differential dynamic logic.edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser
 Parser for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter
 Pretty printer for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXProblemParser
 Parser for KeYmaera X problem files.kyx
edu.cmu.cs.ls.keymaerax.lemma
 Lemma mechanismedu.cmu.cs.ls.keymaerax.lemma.FileLemmaDB
 Lemma database stored in filesedu.cmu.cs.ls.keymaerax.tools
 Arithmetic backendsedu.cmu.cs.ls.keymaerax.tools.Mathematica
 Mathematica interface for real arithmetic and ODE solver etc.edu.cmu.cs.ls.keymaerax.tools.Z3
 Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.Polya
 Polya interface for real arithmetic.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.DerivationInfo
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface info.References
Full references are provided elsewhere 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, LNCS. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.