trait UnifyUSCalculus extends AnyRef
Automatic unificationbased Uniform Substitution Calculus with indexing. Provides a tactic framework for automatically applying axioms and axiomatic rules by matching inputs against them by unification according to the axiom's AxIndex.
This central collection of unificationbased algorithms for focused proof strategies is the basis for using axioms and axiomatic proof rules in flexible ways. It is also central for deciding upon their succession in proof strategies, e.g., which steps to take next.
The most important algorithms are:  UnifyUSCalculus.useAt() makes use of a (derived) axiom or axiomatic rule in any position and logically transforms the goal to prove what is required for the transformation.  UnifyUSCalculus.chase chains together a sequence of canonical useAt inferences to make a formula disappear (chase it away) as far as possible.
Which part of a (derived) axiom to latch on to during a useAt
is determined by the unification keys in the AxiomInfo.theKey.
Which resulting subexpressions to consider next during a chase
is determined by the recursors in the AxiomInfo.theRecursor.
What unifier is used for the default key is, in turn, determined by AxiomInfo.unifier.
Which (derived) axiom is the canonical one to decompose a given expression is determined by AxIndex.axiomsFor()
Default keys and default recursors and default axiom indices can be overwritten by specifing extra arguments.
This can be useful for noncanonical useAts or chases.
The combination of the UnifyUSCalculus algorithms make it possible to implement a tactic for using an axiom as follows:
useAt(Ax.composeb)
Such a tactic can then be applied in different positions of a sequent, e.g.:
useAt(Ax.composeb)(1) useAt(Ax.composeb)(2) useAt(Ax.composeb)(1, 1::0::Nil)
The combination of the UnifyUSCalculus algorithms also make it possible to implement longer proof strategies. For example, completely chasing away a formula by successively using the canonical axioms on the resulting formulas is:
chase
Applying it at different positions of a sequent proceeds as follows, e.g.:
chase(1) chase(2) chase(1, 1::0::Nil)
 See also
AxiomInfo
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017. arXiv:1601.06183
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.
 Alphabetic
 By Inheritance
 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.

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

type
Subst = RenUSubst
The (generalized) substitutions used for unification
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))
 To do
likewise for Context[Term] using CT instead.
 See also
CE(PosInExpr
CEat(Provable)
CMon(Context)

def
CE(inEqPos: PosInExpr): InputTactic
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.
 Annotations
 @Tactic( x$88 , x$87 , x$89 , x$85 , x$86 , x$90 , x$91 , x$92 , x$93 , x$94 , x$95 , x$96 )
 See also
UnifyUSCalculus.CE(Context)
UnifyUSCalculus.CQ(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)
UnifyUSCalculus.CEat(Provable)
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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981

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).CE(fact, Context("⎵".asFormula))
is equivalent toCE(fact)
. , 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
. See also
UnifyUSCalculus.CEat(Provable)
useAtImpl()
CE(Context)
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CQ(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)
Examples: 
def
CEat(fact: ProvableSig, key: PosInExpr): BuiltInPositionTactic
CEat replacing
key
with the other expression in the equality/equivalence.CEat replacing
key
with the other expression in the equality/equivalence. @see CEat(ProvableSig) 
def
CEat(fact: ProvableSig): BuiltInPositionTactic
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
CEat(fact)
is equivalent toCEat(fact, Context("⎵".asFormula))
 To do
Optimization: Would direct propositional rules make CEat faster at pos.isTopLevel?
 See also
UnifyUSCalculus.CEat(Provable,Context)
useAtImpl()
CE(Context)
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CQ(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)
Example: 
def
CEimp(inEqPos: PosInExpr): InputTactic
CEimply(pos) at the indicated position within an equivalence reduces contextual implication
C{left}>C{right}
to argument equivalenceleft<>right
.CEimply(pos) at the indicated position within an equivalence reduces contextual implication
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.
 Annotations
 @Tactic( x$99 , x$100 , x$101 , x$97 , x$98 , x$102 , x$103 , x$104 , x$105 , x$106 , x$107 , x$108 )
 See also
UnifyUSCalculus.CE(Context)
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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981

def
CErevimp(inEqPos: PosInExpr): InputTactic
CErevimply(pos) at the indicated position within an equivalence reduces contextual implication
C{left}>C{right}
to argument equivalenceleft<>right
.CErevimply(pos) at the indicated position within an equivalence reduces contextual implication
C{left}>C{right}
to argument equivalenceleft<>right
.q(x) <> p(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.
 Annotations
 @Tactic( x$111 , x$112 , x$113 , x$109 , x$110 , x$114 , x$115 , x$116 , x$117 , x$118 , x$119 , x$120 )
 See also
UnifyUSCalculus.CE(Context)
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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981

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}
 Note
The direction in the conclusion switches for negative polarity C{⎵}
 See also
UnifyUSCalculus.CMon(PosInExpr)
CE(Context)

def
CMon: BuiltInRightTactic
Convenience CMon first hiding other context.
Convenience CMon first hiding other context.
 o > k  for positive C{.} G  C{o} > C{k}, D
 k > o  for negative C{.} G  C{o} > C{k}, D
 Annotations
 @Tactic( x$135 , x$136 , x$137 , x$133 , x$134 , x$138 , x$139 , x$140 , x$141 , x$142 , x$143 , x$144 )
 See also
CMon()

def
CMon(inEqPos: PosInExpr): InputTactic
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. Contextual monotonicity proof rule. o > k  for positive C{.}  C{o} > C{k}
 k > o  for negative C{.}  C{o} > C{k}
 inEqPos
the position *within* the two sides C{.} of the implication at which the context DotFormula happens.
 Annotations
 @Tactic( x$124 , x$123 , x$125 , x$121 , x$122 , x$126 , x$127 , x$128 , x$129 , x$130 , x$131 , x$132 )
 See also
UnifyUSCalculus.CQ(PosInExpr)
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CMon(Context)
UnifyUSCalculus.CEat())

def
CQ(inEqPos: PosInExpr): InputTactic
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.
 Annotations
 @Tactic( x$51 , x$52 , x$53 , x$49 , x$50 , x$54 , x$55 , x$56 , x$57 , x$58 , x$59 , x$60 )
 See also
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)

def
CQimp(inEqPos: PosInExpr): InputTactic
CQimply(pos) at the indicated position within an equivalence reduces contextual implication
p(left)>p(right)
to argument equalityleft=right
.CQimply(pos) at the indicated position within an equivalence reduces contextual implication
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.
 Annotations
 @Tactic( x$63 , x$64 , x$65 , x$61 , x$62 , x$66 , x$67 , x$68 , x$69 , x$70 , x$71 , x$72 )
 See also
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)

def
CQrevimp(inEqPos: PosInExpr): InputTactic
CQrevimp(pos) at the indicated position within an equivalence reduces contextual implication
p(left)>p(right)
to argument equalityleft=right
.CQrevimp(pos) at the indicated position within an equivalence reduces contextual implication
p(left)>p(right)
to argument equalityleft=right
. This tactic will use CEat() under the hood as needed.g(x) = f(x)  CQ c(f(x)) > c(g(x))
 inEqPos
the position *within* the two sides of the equivalence at which the context DotTerm happens.
 Annotations
 @Tactic( x$75 , x$76 , x$77 , x$73 , x$74 , x$78 , x$79 , x$80 , x$81 , x$82 , x$83 , x$84 )
 See also
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)

def
US(fact: ProvableSig): BuiltInTactic
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.
 See also
byUS()

def
US(subst: USubst): BuiltInTactic
US(subst) uses a uniform substitution of rules to transform an entire provable.
US(subst) uses a uniform substitution of rules to transform an entire provable.
G1  D1 ... Gn  Dn s(G1)  s(D1) ... s(Gn)  s(Dn)  =>  (USR) G  D s(G)  s(D)
 subst
The uniform substitution
s
(of no free variables) to be used on the premises and conclusion of the provable.
 See also
edu.cmu.cs.ls.keymaerax.core.Provable.apply(USubst)
ProvableInfo)

def
US(subst: USubst, fact: ProvableSig): BuiltInTactic
US(subst, fact) reduces the present proof to a proof of
fact
, whose uniform substitution instance undersubst
the current goal is.US(subst, fact) reduces the present proof to a proof of
fact
, whose uniform substitution instance undersubst
the current goal is.s(g1)  s(d1) ... s(gn)  s(dn) g1  d1 ... gn  dn  if  fact G  D g  d where G=s(g) and D=s(d)
 subst
the substitution
s
that instantiates factg  d
to the present goalG  D
. fact
the fact
g  d
to reduce the proof to. Facts do not have to be proved yet.
 See also
edu.cmu.cs.ls.keymaerax.core.Provable.apply(USubst)
ProvableInfo)

def
US(subst: USubst, fact: ProvableInfo): BuiltInTactic
US(subst, fact) reduces the proof to the given fact, whose uniform substitution instance under
subst
the current goal is.US(subst, fact) reduces the proof to the given fact, whose uniform substitution instance under
subst
the current goal is. Whenfact
is an axiom:* *  if  fact G  D g  d where G=s(g) and D=s(d)
When
fact
is an axiomatic rule:s(g1)  s(d1) ... s(gn)  s(dn) g1  d1 ... gn  dn  if  fact G  D g  d where G=s(g) and D=s(d)
 subst
the substitution
s
that instantiates factg  d
to the present goalG  D
. fact
the provable for the axiom
g  d
to reduce the proof to (accordingly for axiomatic rules).
 See also
US(USubst,ProvableSig)

def
USX(S: List[SubstitutionPair]): InputTactic
 Annotations
 @Tactic( x$37 , x$38 , x$41 , x$40 , x$39 , x$42 , x$43 , x$44 , x$45 , x$46 , x$47 , x$48 )

final
def
asInstanceOf[T0]: T0
 Definition Classes
 Any

def
boundRename(what: Variable, repl: Variable): BuiltInPositionTactic
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). 
def
by(lemma: Lemma, subst: Subst): BelleExpr
by(name,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.
 def by(lemma: Lemma, subst: USubst): BelleExpr
 def by(pi: ProvableInfo, subst: Subst): BelleExpr

def
by(pi: ProvableInfo, subst: USubst): BelleExpr
by(pi,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.
by(pi,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
 pi
the provable to use to prove the sequent
 subst
what substitution
s
to use for instantiating the factpi
.
 See also
byUS()
 def by(lemma: Lemma): BelleExpr

def
by(pi: ProvableInfo): BelleExpr
by(pi) uses the given provable with its information literally to continue or close the proof (if it fits to what has been proved).
by(pi) uses the given provable with its information literally to continue or close the proof (if it fits to what has been proved).
 pi
the information for the Provable to use, e.g., from Ax.

def
byUS(pi: ProvableInfo, inst: (Subst) ⇒ Subst): BelleExpr
rule(pi,inst) uses the given axiom or axiomatic rule to prove the sequent.
rule(pi,inst) uses the given axiom or 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.
 pi
the provable info for 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 modify the unifier if other cases than the mostgeneral unifier are preferred.
 See also
byUS()
by()

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

def
byUS(provable: ProvableSig): BuiltInTactic
byUS(pi) proves by a uniform substitution instance of provable (information), obtained by unification with the current goal.
byUS(pi) proves by a uniform substitution instance of provable (information), obtained by unification with the current goal. Like by(ProvableInfo,USubst) except that the required substitution is automatically obtained by unification.
 See also
UnifyUSCalculus.US()

def
byUS(pi: ProvableInfo): BelleExpr
byUS(pi) proves by a uniform substitution instance of provable (information) or axiom or axiomatic rule, obtained by unification with the current goal.
byUS(pi) proves by a uniform substitution instance of provable (information) or axiom or axiomatic rule, obtained by unification with the current goal. Like by(ProvableInfo,USubst) except that the required substitution is automatically obtained by unification.
 See also
UnifyUSCalculus.US()

def
chase(keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst = ax=>us=>us, index: (ProvableInfo) ⇒ (PosInExpr, List[PosInExpr]) = AxIndex.axiomIndex): BuiltInPositionTactic
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. Defaults to AxIndex.axiomFor().
 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. Defaults to identity transformation, i.e., no modification in found match.
 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 AxIndex.axiomIndex.
When applied at 1::Nil, turns [{x'=22}](2*x+x*y>=5)' into [{x'=22}]2*x'+(x'*y+x*y')>=0
, 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}][?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into [{x'=22}]((x>0>x+1>=1) & (x=0>1>=1))
 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[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic): BuiltInPositionTactic
 def chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo]): BuiltInPositionTactic

def
chase(breadth: Int, giveUp: Int): BuiltInPositionTactic
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.

val
chase: BuiltInPositionTactic
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.chaseAt will not branch or use propositional rules, merely transform the chosen formula in place.
 Annotations
 @Tactic( x$2 , x$3 , x$1 , x$4 , x$5 , x$6 , x$7 , x$8 , x$9 , x$10 , x$11 , x$12 )

def
chaseCustom(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): BuiltInPositionTactic
chaseCustom: Unrestricted form of chase where AxiomIndex is not built in, i.e.
chaseCustom: Unrestricted form of chase where AxiomIndex is not built in, i.e. it takes keys of the form Expression => List[(Provable,PosInExpr, List[PosInExpr])] This allows customized rewriting using provables derived at runtime
 def chaseCustomFor(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): ForwardPositionTactic

def
chaseFor(keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst = ax=>us=>us, index: (ProvableInfo) ⇒ (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 axioms/tactics to be used for those expressions. The first applicable axiom/tactic will be chosen. Defaults to AxIndex.axiomIndex.
 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. Defaults to identity transformation, i.e., no modification in found match.
 inst
Transformation for instantiating additional unmatched symbols that do not occur when using the given axiom. 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
The key and recursor information determining (as in AxiomInfo)
._1
which subexpression of the ProvableInfo to match against.._2
which resulting recursors to continue chasing after in the resulting expression. Defaults to AxIndex.axiomIndex.
When applied at 1::Nil, turns [{x'=22}](2*x+x*y>=5)' into [{x'=22}]2*x'+(x'*y+x*y')>=0
, 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}][?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into [{x'=22}]((x>0>x+1>=1) & (x=0>1>=1))
 Note
Chase is searchfree and, thus, quite efficient. It directly follows the axiom index information to compute followup positions for the chase.
 See also
chase()
Examples:  def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst, index: (ProvableInfo) ⇒ (PosInExpr, List[PosInExpr])): ForwardPositionTactic
 def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst): ForwardPositionTactic
 def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic): ForwardPositionTactic
 def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst, index: (ProvableInfo) ⇒ (PosInExpr, List[PosInExpr])): BuiltInPositionTactic
 def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst): BuiltInPositionTactic
 def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst): BuiltInPositionTactic

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

def
cutAt(repl: Expression): DependentPositionWithAppliedInputTactic
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
 Annotations
 @Tactic( x$147 , x$148 , x$149 , x$145 , x$146 , x$150 , x$151 , x$152 , x$153 , x$154 , x$155 , x$156 )
 See also
UnifyUSCalculus.CEat(Provable)

val
deepChase: BuiltInPositionTactic
Chases the expression at the indicated position forward.
Chases the expression at the indicated position forward. Unlike chase descends into formulas and terms exhaustively.
 Annotations
 @Tactic( x$14 , x$15 , x$13 , x$16 , x$17 , x$18 , x$19 , x$20 , x$21 , x$22 , x$23 , x$24 )

def
either(left: ForwardTactic, right: ForwardTactic): ForwardTactic
either(left,right) runs
left
if successful andright
otherwise (for forward tactics). 
def
eitherP(left: ForwardPositionTactic, right: ForwardPositionTactic): ForwardPositionTactic
eitherP(left,right) runs
left
if successful andright
otherwise (for forward tactics). 
final
def
eq(arg0: AnyRef): Boolean
 Definition Classes
 AnyRef

def
equals(arg0: Any): Boolean
 Definition Classes
 AnyRef → Any

val
fail: BuiltInTactic
fail is a tactic that always fails as being inapplicable
fail is a tactic that always fails as being inapplicable
 Annotations
 @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
 See also

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

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

def
ifThenElse(cond: (ProvableSig) ⇒ Boolean, thenT: ForwardTactic, elseT: ForwardTactic): ForwardTactic
ifThenElse(cond,thenT,elseT) runs
thenT
ifcond
holds andelseT
otherwise (for forward tactics). 
def
ifThenElseP(cond: (Position) ⇒ (ProvableSig) ⇒ Boolean, thenT: ForwardPositionTactic, elseT: ForwardPositionTactic): ForwardPositionTactic
ifThenElseP(cond,thenT,elseT) runs
thenT
ifcond
holds andelseT
otherwise (for forward tactics). 
final
def
isInstanceOf[T0]: Boolean
 Definition Classes
 Any

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. 
final
def
ne(arg0: AnyRef): Boolean
 Definition Classes
 AnyRef

val
nil: BuiltInTactic
nil=skip is a noop tactic that has no effect
nil=skip is a noop tactic that has no effect
 Annotations
 @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )

final
def
notify(): Unit
 Definition Classes
 AnyRef
 Annotations
 @native()

final
def
notifyAll(): Unit
 Definition Classes
 AnyRef
 Annotations
 @native()

def
seqCompose(first: ForwardTactic, second: ForwardTactic): ForwardTactic
seqCompose(first,second) runs
first
followed bysecond
(for forward tactics). 
def
seqComposeP(first: ForwardPositionTactic, second: ForwardPositionTactic): ForwardPositionTactic
seqComposeP(first,second) runs
first
followed bysecond
(for forward tactics). 
val
skip: BuiltInTactic
skip is a noop tactic that has no effect Identical to nil but different name
skip is a noop tactic that has no effect Identical to nil but different name
 Annotations
 @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
 See also

def
stepAt(axiomIndex: (Expression) ⇒ Option[DerivationInfo]): 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 AxIndex.
 Note
Efficient sourcelevel indexing implementation.
 See also

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

def
toString(): String
 Definition Classes
 AnyRef → Any

val
todo: BuiltInTactic
A noop tactic that as no effect but marks an open proof task.
A noop tactic that as no effect but marks an open proof task.
 Annotations
 @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
 See also

def
uniformRename(ur: URename): BuiltInTactic
uniformRename(ur) renames
ur.what
tour.repl
uniformly and vice versa.uniformRename(ur) renames
ur.what
tour.repl
uniformly and vice versa. 
def
uniformRename(what: Variable, repl: Variable): BuiltInTactic
uniformRename(what,repl) renames
what
torepl
uniformly and vice versa.uniformRename(what,repl) renames
what
torepl
uniformly and vice versa. 
def
uniformRenameF(what: Variable, repl: Variable): ForwardTactic
uniformRenameF(what,repl) renames
what
torepl
uniformly (for forward tactics). 
def
uniformSubstitute(subst: USubst): InputTactic
 See also
US()

def
useAt(lem: Lemma): BuiltInPositionTactic
useAt(lem)(pos) uses the given lemma at the given position in the sequent (by unifying and equivalence rewriting).
 def useAt(lem: Lemma, key: PosInExpr): BuiltInPositionTactic

def
useAt(lem: Lemma, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): BuiltInPositionTactic
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.
 inst
optional transformation augmenting or replacing the uniform substitutions after unification with additional information.

def
useAt(axiom: ProvableInfo, key: PosInExpr): BuiltInPositionTactic
useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), overwriting key.
useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), overwriting key.
 key
the optional position of the key in the axiom to unify with.

def
useAt(axiom: AxiomInfo, inst: (Option[Subst]) ⇒ Subst): BuiltInPositionTactic
useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), with a given instantiation augmentation.
useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), with a given instantiation augmentation.
 inst
transformation augmenting or replacing the uniform substitutions after unification with additional information.

def
useAt(axiom: ProvableInfo, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): BuiltInPositionTactic
useAt(axiom)(pos) uses the given axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence/implicational rewriting).
useAt(axiom)(pos) uses the given axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence/implicational rewriting). Unifies the left or right part of fact with what's found at sequent(pos) and use corresponding instance to make progress by reducing to the other side.
G  C{s(r)}, D  useAt(__l__<>r) if s=unify(c,l) G  C{c}, D
and accordingly for implication facts that are
l>r
facts or conditional equivalencesp>(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.Backward Tableauxstyle proof analogue of useFor().
Tactic specification:
useAt(fact)(p)(F) = let (C,c)=F(p) in case c of { s=unify(fact.left,_) => CutRight(C(s(fact.right))(p) ; <( "use cut": skip "show cut": EquivifyRight(p.top) ; CoHide(p.top) ; CE(C(_)) ; fact ) s=unify(fact.right,_) => accordingly with an extra commuteEquivRightT }
 axiom
describing what fact to use to simplify at the indicated position of the sequent
 key
the part of the Formula fact to unify the indicated position of the sequent with
 inst
Transformation for instantiating additional unmatched symbols that do not occur in fact(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.
useAt(AxiomInfo("[;] choice", PosInExpr(0::Nil))(0, PosInExpr(1::1::Nil)) applied to the indicated 1::1::Nil position of [x:=1;][{x'=22}] [x:=2*x;++x:=0;]x>=0 turns it into [x:=1;][{x'=22}] ([x:=2*x;]x>=0 & [x:=0;]x>=0)
 To do
could directly use prop rules instead of CE if key close to HereP if more efficient.
 See also
useFor()
Example: 
def
useAt(axiom: ProvableInfo): BuiltInPositionTactic
useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting).

def
useExpansionAt(axiom: AxiomInfo): BuiltInPositionTactic
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.
 See also
useAt(AxiomInfo)

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 useAtImpl().
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 useAtImpl().
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.
useFor(Axiom.axiom(Ax.composeb), 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
useAtImpl()
Example:  def useFor(axiom: ProvableInfo, inst: (Subst) ⇒ Subst): ForwardPositionTactic

def
useFor(pi: ProvableInfo, key: PosInExpr, inst: (Subst) ⇒ Subst): ForwardPositionTactic
useFor(pi, key) use the key part of the given axiom or provable info forward for the selected position in the given Provable to conclude a new Provable
useFor(pi, key) use the key part of the given axiom or provable info 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 AxiomInfo.theKey
 inst
optional transformation augmenting or replacing the uniform substitutions after unification with additional information. Defaults to no change.
 def useFor(axiom: ProvableInfo, key: PosInExpr): ForwardPositionTactic

def
useFor(axiom: ProvableInfo): ForwardPositionTactic
useFor(axiom) use the given (derived) axiom/axiomatic rule forward for the selected position in the given Provable to conclude a new Provable

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( ... )
Deprecated Value Members

def
by(fact: ⇒ ProvableSig, name: String = TacticFactory.ANON): 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)
 fact
the Provable to drop into the proof to proceed or close it if proved.
 name
the name to use/record for the tactic
 Annotations
 @deprecated
 Deprecated
use by(ProvableInfo) instead if possible.
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