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 AxiomIndex.
 See also
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. arXiv:1601.06183
 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
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.
 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).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
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}
 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.

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.
 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.
 See also
UnifyUSCalculus.CMon(PosInExpr)
UnifyUSCalculus.CE(PosInExpr)

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

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. 
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. See also
edu.cmu.cs.ls.keymaerax.core.Provable.apply(USubst)

final
def
asInstanceOf[T0]: T0
 Definition Classes
 Any

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

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
.
 See also
byUS()
 def by(lemma: Lemma, name: String): BelleExpr

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)

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)

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.
 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.
 See also
UnifyUSCalculus.byUS()

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

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.
 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.
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
 def chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String]): DependentPositionTactic

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.

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.

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
 def chaseCustomFor(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): ForwardPositionTactic

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.
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
 def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst): ForwardPositionTactic
 def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic): ForwardPositionTactic
 def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst, index: (String) ⇒ (PosInExpr, List[PosInExpr])): DependentPositionTactic
 def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst): DependentPositionTactic
 def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], inst: (String) ⇒ (Subst) ⇒ Subst): DependentPositionTactic

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): 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
 See also
UnifyUSCalculus.CEat(Provable)

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

def
finalize(): Unit
 Attributes
 protected[java.lang]
 Definition Classes
 AnyRef
 Annotations
 @throws( classOf[java.lang.Throwable] )
 def fromAxIndex(s: String): (ProvableSig, PosInExpr, List[PosInExpr])

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 lazyUseAt(lemmaName: String, key: PosInExpr): DependentPositionTactic

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

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

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). 
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.
 Note
Efficient sourcelevel indexing implementation.
 See also

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

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. 
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. 
def
uniformRenameF(what: Variable, repl: Variable): ForwardTactic
uniformRenameF(what,repl) renames
what
torepl
uniformly (for forward tactics). 
def
uniformSubstitute(subst: USubst): BuiltInTactic
 See also
US()
 def useAt(axiom: ProvableInfo, key: PosInExpr): DependentPositionTactic
 def useAt(axiom: ProvableInfo, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic

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).
 def useAt(axiom: String, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
 def useAt(axiom: String, key: PosInExpr): DependentPositionTactic

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.

def
useAt(lem: Lemma): DependentPositionTactic
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): DependentPositionTactic

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.
 def useExpansionAt(axiom: String, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic

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.

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.

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

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

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

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