object TactixLibrary extends HilbertCalculus with SequentCalculus
Tactix: Main tactic library with simple interface. This library features all main tactics for the most common cases.
For tactics implementing builtin rules such as sequent proof rules, elaborate documentation can be found in the prover kernel.
Main search tactics that combine numerous other tactics for automation purposes include:
 TactixLibrary.master automatic proof search
 TactixLibrary.auto automatic proof search if that successfully proves the given property
 TactixLibrary.normalize normalize to sequent normal form
 TactixLibrary.unfoldProgramNormalize normalize to sequent normal form, avoiding unnecessary branching
 TactixLibrary.prop propositional logic proving
 TactixLibrary.QE prove real arithmetic
 TactixLibrary.ODE proving properties of differential equations
 TactixLibrary.step performs one canonical simplifying proof step
 TactixLibrary.chase chase the given formula away by automatic reduction proofs
The tactic library also includes individual proof calculi:
 HilbertCalculus: Hilbert Calculus for differential dynamic logic.
 SequentCalculus: Sequent Calculus for propositional and firstorder logic.
 UnifyUSCalculus: Automatic unificationbased Uniform Substitution Calculus with indexing.
 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.
 Alphabetic
 By Inheritance
 TactixLibrary
 SequentCalculus
 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

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.
 Definition Classes
 HilbertCalculus
 See also
Figure 3 in Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 2016.

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)
.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)
. Definition Classes
 HilbertCalculus

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)
.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)
. Definition Classes
 HilbertCalculus

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
 Definition Classes
 HilbertCalculus
 [{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
DGauto: DependentPositionTactic
DG/DA differential ghosts that are generated automatically to prove differential equations.
DG/DA differential ghosts that are generated automatically to prove differential equations.
 See also

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)'
. Definition Classes
 HilbertCalculus
 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))
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))
 Definition Classes
 HilbertCalculus

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))
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))
 Definition Classes
 HilbertCalculus

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))
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))
 Definition Classes
 HilbertCalculus

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

val
G: DependentPositionTactic
G: Gödel generalization rule reduces a proof of
 [a]p(x)
to proving the postcondition p(x)
in isolation.G: Gödel generalization rule reduces a proof of
 [a]p(x)
to proving the postcondition p(x)
in isolation. p()  G G  [a]p(), D
The more flexible and more general rule monb with p(x)=True gives
G
using boxTrue. Definition Classes
 HilbertCalculus
 Note
Unsound for hybrid games
 See also
monb with p(x)=True

lazy val
K: DependentPositionTactic
K: modal modus ponens (hybrid systems)
K: modal modus ponens (hybrid systems)
 Definition Classes
 HilbertCalculus
 Note
Use with care since limited to hybrid systems. Use monb instead.
 See also

lazy val
ODE: DependentPositionTactic
ODE: try to prove a property of a differential equation automatically.
ODE: try to prove a property of a differential equation automatically.
 To do
@see dC
 See also
 def QE: BelleExpr

def
QE(order: Seq[NamedSymbol] = Nil, requiresTool: Option[String] = None, timeout: Option[Int] = None): BelleExpr
QE: Quantifier Elimination to decide real arithmetic (after simplifying logical transformations).

def
RCF: BelleExpr
Realclosed field arithmetic on a single formula without any extra smarts and simplifications.
Realclosed field arithmetic on a single formula without any extra smarts and simplifications.
 See also

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()
. Definition Classes
 HilbertCalculus
 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.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. Definition Classes
 HilbertCalculus

def
abbrv(name: Variable): DependentPositionTactic
abbrv(name) Abbreviate the term at the given position by a new name and use that name at all occurrences of that term.
abbrv(name) Abbreviate the term at the given position by a new name and use that name at all occurrences of that term.
 name
The new variable to use as an abbreviation.
maxcd = max(c,d)  a+b <= maxcd+e abbrv(Variable("maxcd"))(1, 1::0::Nil)  a+b <= max(c, d) + e
Example: 
lazy val
abs: DependentPositionTactic
Expands absolute value using
abs(x)=y <> (x>=0&y=x  x<=0&y=x)
, see EqualityTactics.abs 
lazy val
abstractionb: DependentPositionTactic
abstractionb: turns '[a]p' into \forall BV(a) p by universally quantifying over all variables modified in
a
.abstractionb: turns '[a]p' into \forall BV(a) p by universally quantifying over all variables modified in
a
. Returns a tactic to abstract a box modality to a formula that quantifies over the bound variables in the program of that modality. x>0 abstractionb(1)  [y:=2;]x>0
,  x>0 & z=1 > [z:=y;]\forall x x>0 abstractionb(1, 1::1::Nil)  x>0 & z=1 > [z:=y;][x:=2;]x>0
,  \forall x x>0 abstractionb(1)  [x:=2;]x>0
Examples: 
lazy val
allDist: DependentPositionTactic
 Definition Classes
 HilbertCalculus

lazy val
allG: BelleExpr
allG: all generalization rule reduces a proof of
 \forall x p(x)
to proving p(x)
in isolationallG: all generalization rule reduces a proof of
 \forall x p(x)
to proving p(x)
in isolation Definition Classes
 HilbertCalculus

def
allL(inst: Term): DependentPositionTactic
all left: instantiate a universal quantifier in the antecedent by the concrete instance
term
.all left: instantiate a universal quantifier in the antecedent by the concrete instance
term
. Definition Classes
 SequentCalculus

def
allL(x: Variable, inst: Term): DependentPositionTactic
all left: instantiate a universal quantifier for variable x in the antecedent by the concrete instance
term
.all left: instantiate a universal quantifier for variable x in the antecedent by the concrete instance
term
. Definition Classes
 SequentCalculus

val
allL: DependentPositionTactic
all left: instantiate a universal quantifier in the antecedent by itself.
all left: instantiate a universal quantifier in the antecedent by itself.
 Definition Classes
 SequentCalculus

def
allLPos(instPos: Position): DependentPositionTactic
all left: instantiate a universal quantifier in the antecedent by the term obtained from position
instPos
.all left: instantiate a universal quantifier in the antecedent by the term obtained from position
instPos
. Definition Classes
 SequentCalculus

val
allR: DependentPositionTactic
all right: Skolemize a universal quantifier in the succedent (Skolemize) Skolemization with bound renaming on demand.
all right: Skolemize a universal quantifier in the succedent (Skolemize) Skolemization with bound renaming on demand.
 Definition Classes
 SequentCalculus
Uniformly renames other occurrences of the quantified variable in the context on demand.
x_0>0  x^2>=0 allSkolemize(1) x>0  \forall x x^2>=0
, y>5  x^2>=0 allSkolemize(1) y>5  \forall x x^2>=0
 See also
Examples: 
lazy val
allV: DependentPositionTactic
allV: vacuous
\forall x p()
will be discarded and replaced by p() provided x does not occur in p().allV: vacuous
\forall x p()
will be discarded and replaced by p() provided x does not occur in p(). Definition Classes
 HilbertCalculus

lazy val
alphaRule: BelleExpr
Alpha rules are propositional rules that do not split

val
andL: BuiltInLeftTactic
&L And left: split a conjunction in the antecedent into separate assumptions (AndLeft)
&L And left: split a conjunction in the antecedent into separate assumptions (AndLeft)
 Definition Classes
 SequentCalculus

def
andLi(pos1: AntePos = AntePos(0), pos2: AntePos = AntePos(1)): DependentTactic
Inverse of andL.
Inverse of andL.
G, G', G'', a&b  D  G, a, G', b, G''  D
 Definition Classes
 SequentCalculus

val
andLi: DependentTactic
 Definition Classes
 SequentCalculus

val
andR: BuiltInRightTactic
&R And right: prove a conjunction in the succedent on two separate branches (AndRight)
&R And right: prove a conjunction in the succedent on two separate branches (AndRight)
 Definition Classes
 SequentCalculus

final
def
asInstanceOf[T0]: T0
 Definition Classes
 Any

def
assertE(expected: ⇒ Expression, msg: ⇒ String): BuiltInPositionTactic
Assert that the given expression is present at the position in the sequent where this tactic is applied to.

def
assertT(cond: (Sequent, Position) ⇒ Boolean, msg: ⇒ String): BuiltInPositionTactic
Assert that the given condition holds for the sequent at the position where the tactic is applied

def
assertT(antecedents: Int, succedents: Int, msg: ⇒ String = ""): BelleExpr
Assert that the sequent has the specified number of antecedent and succedent formulas, respectively.

def
assertT(cond: (Sequent) ⇒ Boolean, msg: ⇒ String): BelleExpr
Assert that the given condition holds for the goal's sequent.

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. Definition Classes
 HilbertCalculus
 [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 equationassignd: <:=> simplify assignment
<x:=f;>p(x)
by substitutionp(f)
or equation Definition Classes
 HilbertCalculus
 def atomicQE: BelleExpr

def
atomicQE(split: BelleExpr = ..., preQE: BelleExpr = skip, qe: BelleExpr = QE): BelleExpr
Splits propositional into many smallest possible QE calls.
Splits propositional into many smallest possible QE calls.
 split
Configures how the tactic splits into smaller subgoals before QE (default: exhaustive alpha and beta rules).
 preQE
Tactic to execute before each individual QE call (default: skip).
 qe
How to QE

def
auto: BelleExpr
auto: automatically try hard to prove the current goal if that succeeds.
auto: automatically try hard to prove the current goal if that succeeds.
 See also

lazy val
betaRule: BelleExpr
Beta rules are propositional rules that split

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)
.box: [.] to reduce doublenegated diamond
!⟨a⟩!p(x)
to a box[a]p(x)
. Definition Classes
 HilbertCalculus

lazy val
boxAnd: DependentPositionTactic
boxAnd: splits
[a](p&q)
into[a]p & [a]q
boxAnd: splits
[a](p&q)
into[a]p & [a]q
 Definition Classes
 HilbertCalculus

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

val
boxTrue: DependentPositionTactic
boxTrue: proves
[a]true
directly for hybrid systemsa
that are not hybrid games.boxTrue: proves
[a]true
directly for hybrid systemsa
that are not hybrid games. Definition Classes
 HilbertCalculus

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)
choiceb: [++] handles both cases of a nondeterministic choice
[a++b]p(x)
separately[a]p(x) & [b]p(x)
 Definition Classes
 HilbertCalculus

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

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

def
close(a: Int, s: Int): BelleExpr
 Definition Classes
 SequentCalculus

def
close(a: AntePos, s: SuccPos): BelleExpr
close: closes the branch when the same formula is in the antecedent and succedent (Close)
close: closes the branch when the same formula is in the antecedent and succedent (Close)
 Definition Classes
 SequentCalculus

lazy val
close: BelleExpr
close: closes the branch when the same formula is in the antecedent and succedent or true or false close
close: closes the branch when the same formula is in the antecedent and succedent or true or false close
 Definition Classes
 SequentCalculus

val
closeF: BelleExpr
closeF: closes the branch when false is in the antecedent (CloseFalse)
closeF: closes the branch when false is in the antecedent (CloseFalse)
 Definition Classes
 SequentCalculus

val
closeId: DependentTactic
 Definition Classes
 SequentCalculus

val
closeIdWith: DependentPositionTactic
closeId: closes the branch when the same formula is in the antecedent and succedent (Close)
closeId: closes the branch when the same formula is in the antecedent and succedent (Close)
 Definition Classes
 SequentCalculus

val
closeT: BelleExpr
closeT: closes the branch when true is in the succedent (CloseTrue)
closeT: closes the branch when true is in the succedent (CloseTrue)
 Definition Classes
 SequentCalculus

val
cohide: DependentPositionTactic
CoHide/coweaken whether left or right: drop all other formulas from the sequent (CoHideLeft)
CoHide/coweaken whether left or right: drop all other formulas from the sequent (CoHideLeft)
 Definition Classes
 SequentCalculus

def
cohide2: BuiltInTwoPositionTactic
CoHide2/coweaken2 both left and right: drop all other formulas from the sequent (CoHide2)
CoHide2/coweaken2 both left and right: drop all other formulas from the sequent (CoHide2)
 Definition Classes
 SequentCalculus

val
cohideL: BuiltInLeftTactic
CoHide/weaken left: drop all other formulas from the sequent (CoHideLeft)
CoHide/weaken left: drop all other formulas from the sequent (CoHideLeft)
 Definition Classes
 SequentCalculus

def
cohideOnlyL: DependentPositionTactic
Cohides in antecedent, but leaves succedent as is.
Cohides in antecedent, but leaves succedent as is.
 Definition Classes
 SequentCalculus

def
cohideOnlyR: DependentPositionTactic
Cohides in succedent, but leaves antecedent as is.
Cohides in succedent, but leaves antecedent as is.
 Definition Classes
 SequentCalculus

val
cohideR: BuiltInRightTactic
CoHide/weaken right: drop all other formulas from the sequent (CoHideRight)
CoHide/weaken right: drop all other formulas from the sequent (CoHideRight)
 Definition Classes
 SequentCalculus

lazy val
commuteEqual: DependentPositionTactic
Commute equality
a=b
tob=a
Commute equality
a=b
tob=a
 Definition Classes
 SequentCalculus

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

val
commuteEquivL: BuiltInLeftTactic
Commute equivalence on the left CommuteEquivLeft
Commute equivalence on the left CommuteEquivLeft
 Definition Classes
 SequentCalculus

val
commuteEquivR: BuiltInRightTactic
Commute equivalence on the right CommuteEquivRight
Commute equivalence on the right CommuteEquivRight
 Definition Classes
 SequentCalculus

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

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

def
con(v: Variable, variant: Formula, pre: BelleExpr = SaturateTactic(alphaRule)): DependentPositionWithAppliedInputTactic
Loop convergence: prove a diamond property of a loop by induction with a variant for progress.
Loop convergence: prove a diamond property of a loop by induction with a variant for progress.
init: use: step: G  exists v. J(v), D v<=0, J(v), consts  p v>0, J(v), consts  <a>J(v1)  G  <{a}*>p, D
 variant
The variant property or convergence property in terms of new variable
v
.
The variant J(v) ~> (v = z) is specified as v=="v".asVariable, variant == "v = z".asFormula
Example: 
def
cut(cut: Formula): InputTactic
cut a formula in to prove it on one branch and then assume it on the other.
cut a formula in to prove it on one branch and then assume it on the other. Or to perform a case distinction on whether it holds (Cut)
 Definition Classes
 SequentCalculus

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)

def
cutL(cut: Formula): DependentPositionWithAppliedInputTactic
cut a formula in in place of pos on the left to prove it on one branch and then assume it on the other.
cut a formula in in place of pos on the left to prove it on one branch and then assume it on the other. (CutLeft)
 Definition Classes
 SequentCalculus

def
cutLR(cut: Formula): DependentPositionWithAppliedInputTactic
cut a formula in in place of pos to prove it on one branch and then assume it on the other (whether pos is left or right).
cut a formula in in place of pos to prove it on one branch and then assume it on the other (whether pos is left or right). (CutLeft or CutRight)
 Definition Classes
 SequentCalculus

def
cutR(cut: Formula): DependentPositionWithAppliedInputTactic
cut a formula in in place of pos on the right to prove it on one branch and then assume it on the other.
cut a formula in in place of pos on the right to prove it on one branch and then assume it on the other. (CutRight)
 Definition Classes
 SequentCalculus

def
dC(formulas: Formula*): DependentPositionTactic
DC: Differential Cut a new invariant, use old(x) to refer to initial values of variable x.
DC: Differential Cut a new invariant, use old(x) to refer to initial values of variable x. Use special function old(.) to introduce a discrete ghost for the starting value of a variable that can be used in the evolution domain constraint.
 formulas
the list of formulas that will be cut into the differential equation in that order. The formulas are typically shown to be differential invariants subsequently. They can use old(x) and old(y) etc. to refer to the initial values of x and y, respectively.
x>0, v>=0, x_0=x  [{x'=v,v'=1&v>=0&x>=x_0}]x>=0 x>0, v>=0  [{x'=v,v'=1}]v>=0 x>0, v>=0, x_0=x  [{x'=v,v'=1&v>=0}]x>=x_0 diffCut("v>=0".asFormula, "x>=old(x)".asFormula)(1) x>0, v>=0  [{x'=v,v'=1}]x>=0
, x>0, x_0=x  [{x'=2&x>=x_0}]x>=0 x>0, x_0=x  [{x'=2}]x>=x_0 diffCut("x>=old(x)".asFormula)(1) x>0  [{x'=2}]x>=0
, x>0  [{x'=2&x>0}]x>=0 x>0  [{x'=2}]x>0 diffCut("x>0".asFormula)(1) x>0  [{x'=2}]x>=0
 Note
diffCut is often needed when FV(post) depend on BV(ode) that are not in FV(constraint).
 See also
diffInvariant()
Examples: 
def
dG(ghost: DifferentialProgram, r: Option[Formula]): DependentPositionTactic
dG(ghost,r): Differential Ghost add auxiliary differential equations with extra variables ghost of the form y'=a*y+b and the postcondition replaced by r, if provided.
dG(ghost,r): Differential Ghost add auxiliary differential equations with extra variables ghost of the form y'=a*y+b and the postcondition replaced by r, if provided.
G  \exists y [x'=f(x),y'=g(x,y)&q(x)]r(x,y), D  dG using p(x) <> \exists y. r(x,y) by QE G  [x'=f(x)&q(x)]p(x), D
 ghost
the extra differential equation for an extra variable y to ghost in of the form y'=a*y+b or y'=a*y or y'=b or y'=a*yb
 r
the optional equivalent new postcondition to prove that can mention y; keeps p(x) if omitted.
proveBy("x>0>[{x'=x}]x>0".asFormula, implyR(1) & dG("{y'=(1/2)*y}".asDifferentialProgram, Some("x*y^2=1".asFormula))(1) & diffInd()(1, 0::Nil) & QE )
with optional instantiation of initial y
proveBy("x>0>[{x'=x}]x>0".asFormula, implyR(1) & dG("{y'=(1/2)*y}".asDifferentialProgram, Some("x*y^2=1".asFormula))(1) & existsR("1/x^(1/2)".asFormula)(1) & diffInd()(1) & QE )
 Note
Uses QE to prove p(x) <> \exists y. r(x,y)
Example: 
def
dI(auto: Symbol = 'full): DependentPositionTactic
dI: Differential Invariant proves a formula to be an invariant of a differential equation (with the usual steps to prove it invariant) (uses DI, DW, DE, QE)
dI: Differential Invariant proves a formula to be an invariant of a differential equation (with the usual steps to prove it invariant) (uses DI, DW, DE, QE)
 auto
One of 'none, 'diffInd, 'full. Whether or not to automatically close and use DE, DW. 'full: tries to close everything after diffInd rule
*  G  [x'=f(x)&q(x)]p(x), D
'none: behaves as DI rule per cheat sheet
G, q(x)  p(x), D G, q(x)  [x'=f(x)&q(x)](p(x))', D  G  [x'=f(x)&q(x)]p(x), D
'diffInd: behaves as diffInd rule per cheat sheet
G, q(x)  p(x), D q(x)  [x':=f(x)]p(x') @note derive on (p(x))' already done  G  [x'=f(x)&q(x)]p(x), D
proveBy("x^2>=2>[{x'=x^3}]x^2>=2".asFormula, implyR(1) & diffInd()(1) & QE )
, x>=5  [x:=x+1;](true > x>=5&2>=0) diffInd(qeTool, 'full)(1, 1::Nil) x>=5  [x:=x+1;][{x'=2}]x>=5
, x>=5, true  x>=5 x>=5, true  [{x'=2}](x>=5)' diffInd(qeTool, 'none)(1) x>=5  [{x'=2}]x>=5
, x>=5, true  x>=5 true  [{x':=2}]x'>=0 diffInd(qeTool, 'diffInd)(1) x>=5  [{x'=2}]x>=5
, * diffInd(qeTool, 'full)(1) x>=5  [{x'=2}]x>=5
Examples: 
def
dR(formula: Formula, hide: Boolean = true): DependentPositionTactic
Refine toplevel antecedent/succedent ODE domain constraint G [x'=f(x)&R]P, D G [x'=f(x)&Q]R, (D)?  dR G [x'=f(x)&Q]P, D
Refine toplevel antecedent/succedent ODE domain constraint G [x'=f(x)&R]P, D G [x'=f(x)&Q]R, (D)?  dR G [x'=f(x)&Q]P, D
 formula
the formula R to refine Q to
 hide
whether to keep the extra succedents (D) around (default true), which makes position management easier

lazy val
dW: DependentPositionTactic
DW: Differential Weakening uses evolution domain constraint so
[{x'=f(x)&q(x)}]p(x)
reduces to\forall x (q(x)>p(x))
.DW: Differential Weakening uses evolution domain constraint so
[{x'=f(x)&q(x)}]p(x)
reduces to\forall x (q(x)>p(x))
. Note
FV(post)/\BV(x'=f(x)) subseteq FV(q(x)) usually required to have a chance to succeed.

def
debug(s: ⇒ Any): BuiltInTactic
debug(s) sprinkles debug message s into the output and the ProofNode information

def
debugAt(s: ⇒ Any): BuiltInPositionTactic
debugAt(s) sprinkles debug message s into the output and the ProofNode information

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).
 Definition Classes
 HilbertCalculus
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)
.diamond: <.> reduce doublenegated box
![a]!p(x)
to a diamond⟨a⟩p(x)
. Definition Classes
 HilbertCalculus

lazy val
diamondOr: DependentPositionTactic
diamondOr: splits
⟨a⟩(pq)
into⟨a⟩p  ⟨a⟩q
diamondOr: splits
⟨a⟩(pq)
into⟨a⟩p  ⟨a⟩q
 Definition Classes
 HilbertCalculus

def
diffInvariant(invariants: Formula*): DependentPositionTactic
DC+DI: Prove the given list of differential invariants in that order by DC+DI via dC followed by dI Combines differential cut and differential induction.
DC+DI: Prove the given list of differential invariants in that order by DC+DI via dC followed by dI Combines differential cut and differential induction. Use special function old(.) to introduce a ghost for the starting value of a variable that can be used in the evolution domain constraint. Uses diffInd to prove that the formulas are differential invariants. Fails if diffInd cannot prove invariants.
 invariants
The differential invariants to cut in as evolution domain constraint.
x>0, v>=0, x_0=x  [{x'=v,v'=1 & v>=0&x>x_0}]x>=0 diffInvariant("v>=0".asFormula, "x>old(x)".asFormula)(1) x>0, v>=0  [{x'=v,v'=1}]x>=0
, x>0, x_0=x  [{x'=2&x>x_0}]x>=0 diffInvariant("x>old(x)".asFormula)(1) x>0  [{x'=2}]x>=0
, x>0  [{x'=2&x>0}]x>=0 diffInvariant("x>0".asFormula)(1) x>0  [{x'=2}]x>=0
 See also
Examples: 
def
diffVar: DependentPositionTactic
DV: Differential Variant proves a formula to become true at some point after a differential equation.
DV: Differential Variant proves a formula to become true at some point after a differential equation.
*  DV(1) a()>0  <{x'=a()}>x>=b()
Example: 
def
discreteGhost(t: Term, ghost: Option[Variable] = None): DependentPositionTactic
iG discreteGhost: introduces a discrete ghost called
ghost
defined as termt
; ifghost
is None the tactic chooses a name by inspectingt
.iG discreteGhost: introduces a discrete ghost called
ghost
defined as termt
; ifghost
is None the tactic chooses a name by inspectingt
.G, y=e  p(y), D iG (where y is new) G  p(x), D
 t
The ghost's initial value.
 ghost
The new ghost variable. If
None
, the tactic chooses a name by inspecting t (must be a variable then). For robustness you are advised to choose a name.
 [z:=2;][y:=5;]x>0 discreteGhost("0".asTerm, Some("y".asVariable))(1, 1::Nil)  [z:=2;]x>0
,  [y_0:=y;]x>0 discreteGhost("y".asTerm)(1)  x>0
Examples: 
val
done: BelleExpr
done: check that the current goal is proved and fail if it isn't.
done: check that the current goal is proved and fail if it isn't.
 See also

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

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

def
edit(to: Expression): DependentPositionTactic
Determines difference between expression at position and expression
to
and turns diff.Determines difference between expression at position and expression
to
and turns diff. into transformations and abbreviations. 
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 eqL2R(eqPos: AntePosition): DependentPositionTactic

def
eqL2R(eqPos: Int): DependentPositionTactic
Rewrites free occurrences of the lefthand side of an equality into the righthand side at a specific position.
Rewrites free occurrences of the lefthand side of an equality into the righthand side at a specific position.
 eqPos
The position of the equality. If it points to a formula, it rewrites all occurrences of left in that formula. If it points to a specific term, then only this term is rewritten.
x=0  0*y=0, x+1>0 eqL2R(1)(1) x=0  x*y=0, x+1>0
Example:  def eqR2L(eqPos: AntePosition): DependentPositionTactic

def
eqR2L(eqPos: Int): DependentPositionTactic
Rewrites free occurrences of the righthand side of an equality into the lefthand side at a specific position (EqualityTactics.eqR2L).

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

val
equivL: BuiltInLeftTactic
<>L Equiv left: use an equivalence by considering both true or both false cases (EquivLeft)
<>L Equiv left: use an equivalence by considering both true or both false cases (EquivLeft)
 Definition Classes
 SequentCalculus

val
equivR: BuiltInRightTactic
<>R Equiv right: prove an equivalence by proving both implications (EquivRight)
<>R Equiv right: prove an equivalence by proving both implications (EquivRight)
 Definition Classes
 SequentCalculus

val
equivifyR: BuiltInRightTactic
Turn implication on the right into an equivalence, which is useful to prove by CE etc.
Turn implication on the right into an equivalence, which is useful to prove by CE etc. (EquivifyRight)
 Definition Classes
 SequentCalculus

def
errorT(msg: ⇒ String): BuiltInTactic
errorT raises an error upon executing this tactic, stopping processing
 def exhaustiveEqL2R(hide: Boolean = false): DependentPositionTactic

lazy val
exhaustiveEqL2R: DependentPositionTactic
Rewrites free occurrences of the lefthand side of an equality into the righthand side exhaustively (EqualityTactics.exhaustiveEqL2R).
 def exhaustiveEqR2L(hide: Boolean = false): DependentPositionTactic

lazy val
exhaustiveEqR2L: DependentPositionTactic
Rewrites free occurrences of the righthand side of an equality into the lefthand side exhaustively (EqualityTactics.exhaustiveEqR2L).

lazy val
existsE: DependentPositionTactic
 Definition Classes
 HilbertCalculus

val
existsL: DependentPositionTactic
exists left: Skolemize an existential quantifier in the antecedent by introducing a new name for the witness.
exists left: Skolemize an existential quantifier in the antecedent by introducing a new name for the witness.
 Definition Classes
 SequentCalculus

def
existsR(inst: Term): DependentPositionTactic
exists right: instantiate an existential quantifier in the succedent by a concrete instance
inst
as a witnessexists right: instantiate an existential quantifier in the succedent by a concrete instance
inst
as a witness Definition Classes
 SequentCalculus

def
existsR(x: Variable, inst: Term): DependentPositionTactic
exists right: instantiate an existential quantifier for x in the succedent by a concrete instance
inst
as a witnessexists right: instantiate an existential quantifier for x in the succedent by a concrete instance
inst
as a witness Definition Classes
 SequentCalculus

val
existsR: DependentPositionTactic
exists right: instantiate an existential quantifier for x in the succedent by itself as a witness
exists right: instantiate an existential quantifier for x in the succedent by itself as a witness
 Definition Classes
 SequentCalculus

def
existsRPos(instPos: Position): DependentPositionTactic
exists right: instantiate an existential quantifier in the succedent by a concrete term obtained from position
instPos
.exists right: instantiate an existential quantifier in the succedent by a concrete term obtained from position
instPos
. Definition Classes
 SequentCalculus

lazy val
existsV: DependentPositionTactic
existsV: vacuous
\exists x p()
will be discarded and replaced by p() provided x does not occur in p().existsV: vacuous
\exists x p()
will be discarded and replaced by p() provided x does not occur in p(). Definition Classes
 HilbertCalculus

val
fail: BelleExpr
fail is a tactic that always fails
fail is a tactic that always fails
 See also

def
finalize(): Unit
 Attributes
 protected[java.lang]
 Definition Classes
 AnyRef
 Annotations
 @throws( classOf[java.lang.Throwable] )

def
findCounterExample(formula: Formula): Option[Map[NamedSymbol, Expression]]
Finds a counter example, indicating that the specified formula is not valid.

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

def
generalize(C: Formula): DependentPositionTactic
Generalize postcondition to C and, separately, prove that C implies postcondition.
Generalize postcondition to C and, separately, prove that C implies postcondition. The operational effect of {a;b;}@generalize(f1) is generalize(f1).
genUseLbl: genShowLbl: G  [a]C, D C  B  G  [a]B, D
genUseLbl: genShowLbl:  a=2 > [z:=3;][x:=2;]x>1 x>1  [y:=x;]y>1 generalize("x>1".asFormula)(1, 1::1::Nil)  a=2 > [z:=3;][x:=2;][y:=x;]y>1
, genUseLbl: genShowLbl:  [x:=2;]x>1 x>1  [y:=x;]y>1 generalize("x>1".asFormula)(1)  [x:=2;][y:=x;]y>1
Examples: 
final
def
getClass(): Class[_]
 Definition Classes
 AnyRef → Any
 Annotations
 @native()

def
hashCode(): Int
 Definition Classes
 AnyRef → Any
 Annotations
 @native()
 def heuQE: BelleExpr
 def heuQEPO(po: Ordering[Variable]): BelleExpr

val
hide: DependentPositionTactic
Hide/weaken whether left or right
Hide/weaken whether left or right
 Definition Classes
 SequentCalculus

val
hideL: BuiltInLeftTactic
Hide/weaken left: weaken a formula to drop it from the antecedent (HideLeft)
Hide/weaken left: weaken a formula to drop it from the antecedent (HideLeft)
 Definition Classes
 SequentCalculus

val
hideR: BuiltInRightTactic
Hide/weaken right: weaken a formula to drop it from the succcedent (HideRight)
Hide/weaken right: weaken a formula to drop it from the succcedent (HideRight)
 Definition Classes
 SequentCalculus

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: (Sequent, Position) ⇒ Boolean, thenT: BelleExpr, elseT: BelleExpr): DependentPositionTactic
ifThenElse(cond,thenT,elseT) runs
thenT
ifcond
holds at position andelseT
otherwise. 
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

val
implyL: BuiltInLeftTactic
>L Imply left: use an implication in the antecedent by proving its lefthand side on one branch and using its righthand side on the other branch (ImplyLeft)
>L Imply left: use an implication in the antecedent by proving its lefthand side on one branch and using its righthand side on the other branch (ImplyLeft)
 Definition Classes
 SequentCalculus

val
implyR: BuiltInRightTactic
>R Imply right: prove an implication in the succedent by assuming its lefthand side and proving its righthand side (ImplyRight)
>R Imply right: prove an implication in the succedent by assuming its lefthand side and proving its righthand side (ImplyRight)
 Definition Classes
 SequentCalculus

def
implyRi(keep: Boolean = false): BuiltInTwoPositionTactic
Inverse of implyR.
Inverse of implyR.
G, G'  D, D', a > b  G, a, G'  D, b, D'
 Definition Classes
 SequentCalculus

val
implyRi: AppliedBuiltinTwoPositionTactic
 Definition Classes
 SequentCalculus

var
invGenerator: Generator.Generator[Formula]
Default generator for loop invariants and differential invariants to use.
Default generator for loop invariants and differential invariants to use.
 See also

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)
iterateb: [*] prove a property of a loop
[{a}*]p(x)
by unrolling it oncep(x) & [a][{a}*]p(x)
 Definition Classes
 HilbertCalculus

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

def
label(s: String): BelleExpr
Call/label the current proof branch by the toplevel label s.
Call/label the current proof branch by the toplevel label s.
 See also
sublabel()
Idioms.<()

def
label(s: BelleLabel): BelleExpr
Call/label the current proof branch by the given label s.
Call/label the current proof branch by the given label s.
 See also
sublabel()
Idioms.<()

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

def
loop(gen: Generator.Generator[Formula]): DependentPositionTactic
loop: prove a property of a loop by induction, if the given invariant generator finds a loop invariant
loop: prove a property of a loop by induction, if the given invariant generator finds a loop invariant
 See also
loop(Formula)

def
loop(invariant: Formula): DependentPositionTactic
loop: prove a property of a loop by induction with the given loop invariant (hybrid systems) Wipes conditions that contain bound variables of the loop.
loop: prove a property of a loop by induction with the given loop invariant (hybrid systems) Wipes conditions that contain bound variables of the loop.
use: init: step: I, G\BV(a)  p, D\BV(a) G  I, D I, G\BV(a)  [a]p, D\BV(a)  G  [{a}*]p, D
 invariant
The loop invariant
I
.
use: init: step: x>1, y>0  x>0 x>2, y>0  x>1 x>1, y>0  [x:=x+y;]x>1 I("x>1".asFormula)(1) x>2, y>0  [{x:=x+y;}*]x>0
, use: init: step: x>1  x>0 x>2  x>1 x>1  [x:=x+1;]x>1 I("x>1".asFormula)(1) x>2  [{x:=x+1;}*]x>0
 Note
Currently uses I induction axiom, which is unsound for hybrid games.
Examples: 
def
loopPostMaster(gen: Generator.Generator[Formula]): DependentPositionTactic
loopPostMaster: searchandrescue style automatic loop induction based on successive generator gen.
loopPostMaster: searchandrescue style automatic loop induction based on successive generator gen. Uses SearchAndRescueAgain to avoid repetitive proving. Present implementation needs differential equations to occur somewhere within the loop.
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017. Example 32.

def
loopSR(gen: Generator.Generator[Formula]): DependentPositionTactic
loopSR: cleverly prove a property of a loop automatically by induction, trying hard to generate loop invariants.
loopSR: cleverly prove a property of a loop automatically by induction, trying hard to generate loop invariants. Uses SearchAndRescueAgain to avoid repetitive proving.
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017. Example 32.

def
loopauto(gen: Generator.Generator[Formula] = ...): DependentPositionTactic
loop: prove a property of a loop automatically by induction, trying hard to generate loop invariants.
loop: prove a property of a loop automatically by induction, trying hard to generate loop invariants.
 See also
loop(Formula)

def
master(gen: Generator.Generator[Formula] = ..., keepQEFalse: Boolean = true): BelleExpr
master: master tactic that tries hard to prove whatever it could.
master: master tactic that tries hard to prove whatever it could.
keepQEFalse
indicates whether or not a resultfalse
of a QE step at the leaves is kept or undone (i.e., reverted to the QE input sequent). See also

def
master(loop: AtPosition[_ <: BelleExpr], odeR: AtPosition[_ <: BelleExpr], keepQEFalse: Boolean): BelleExpr
Master/auto implementation with tactic
loop
for nondeterministic repetition andodeR
for differential equations in the succedent.Master/auto implementation with tactic
loop
for nondeterministic repetition andodeR
for differential equations in the succedent.keepQEFalse
indicates whether or not QE results "false" at the proof leaves should be kept or undone. 
lazy val
max: DependentPositionTactic
Expands maximum function using
max(x,y)=z <> (x>=y&z=x  x<=y&z=y)
, see EqualityTactics.minmax 
lazy val
min: DependentPositionTactic
Expands minimum function using
min(x,y)=z <> (x<=y&z=x  x>=y&z=y)
, see EqualityTactics.minmax 
def
modusPonens(assumption: AntePos, implication: AntePos): BelleExpr
Modus Ponens: p&(p>q) > q.
Modus Ponens: p&(p>q) > q.
 assumption
Position pointing to p
 implication
Position pointing to p>q
 Definition Classes
 SequentCalculus
p, q, G  D  modusPonens p, p>q, G  D
Example: 
lazy val
monb: BelleExpr
monb: Monotone
[a]p(x)  [a]q(x)
reduces to provingp(x)  q(x)
monb: Monotone
[a]p(x)  [a]q(x)
reduces to provingp(x)  q(x)
 Definition Classes
 HilbertCalculus

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

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

val
nil: BelleExpr
nil=skip is a noop tactic that has no effect

def
normalize(beta: AtPosition[_ <: BelleExpr]*): BelleExpr
Normalize to sequent form.
Normalize to sequent form. Keeps branching factor of tacticChase restricted to
beta
rules. 
lazy val
normalize: BelleExpr
Normalize to sequent form.

val
notL: BuiltInLeftTactic
!L Not left: move an negation in the antecedent to the succedent (NotLeft)
!L Not left: move an negation in the antecedent to the succedent (NotLeft)
 Definition Classes
 SequentCalculus

val
notR: BuiltInRightTactic
!R Not right: move an negation in the succedent to the antecedent (NotRight)
!R Not right: move an negation in the succedent to the antecedent (NotRight)
 Definition Classes
 SequentCalculus

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

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

lazy val
odeInvariant: DependentPositionTactic
Attempts to prove ODE property as an invariant of the ODE directly [LICS'18] G  P P  [x'=f(x)&Q]P  G  [x'=f(x)&Q]P (Default behavior: fast (but incomplete) version, no solving attempted)

lazy val
odeInvariantAuto: DependentPositionTactic
Attemppts to prove ODE property by asking for an automatically generated invariant C from Pegasus, i.e.,
Attemppts to prove ODE property by asking for an automatically generated invariant C from Pegasus, i.e.,
G  C C  [x'=f(x)&Q]C C  P  G  [x'=f(x)&Q]P
(fast version, no solving attempted)

def
onAll(e: BelleExpr): BelleExpr
OnAll(e) == <(e, ..., e) runs tactic
e
on all current branches. 
def
openDiffInd: DependentPositionTactic
DIo: Open Differential Invariant proves an open formula to be an invariant of a differential equation (with the usual steps to prove it invariant) openDiffInd: proves an inequality to be an invariant of a differential equation (by DIo, DW, DE, QE) For strict inequalities, it uses open diff ind (<,>)
DIo: Open Differential Invariant proves an open formula to be an invariant of a differential equation (with the usual steps to prove it invariant) openDiffInd: proves an inequality to be an invariant of a differential equation (by DIo, DW, DE, QE) For strict inequalities, it uses open diff ind (<,>)
proveBy("x^2>9>[{x'=x^4}]x^2>9".asFormula, implyR(1) & openDiffInd()(1) )
, * openDiffInd(1) x^3>5  [{x'=x^3+x^4}]x^3>5
, * openDiffInd(1) x^2>5  [{x'=x^3+x^4}]x^2>5
Examples: 
val
orL: BuiltInLeftTactic
L Or left: use a disjunction in the antecedent by assuming each option on separate branches (OrLeft)
L Or left: use a disjunction in the antecedent by assuming each option on separate branches (OrLeft)
 Definition Classes
 SequentCalculus

val
orR: BuiltInRightTactic
R Or right: split a disjunction in the succedent into separate formulas to show alternatively (OrRight)
R Or right: split a disjunction in the succedent into separate formulas to show alternatively (OrRight)
 Definition Classes
 SequentCalculus

def
orRi(pos1: SuccPos = SuccPos(0), pos2: SuccPos = SuccPos(1)): DependentTactic
Inverse of orR.
Inverse of orR.
G  D, D', D'', a  b  G  D, a, D', b, D''
 Definition Classes
 SequentCalculus

val
orRi: DependentTactic
 Definition Classes
 SequentCalculus

def
partialQE: BelleExpr
Quantifier elimination returning equivalent result, irrespective of result being valid or not.
Quantifier elimination returning equivalent result, irrespective of result being valid or not. Performs QE and allows the goal to be reduced to something that isn't necessarily true.
 Note
You probably want to use fullQE most of the time, because partialQE will destroy the structure of the sequent

def
positionOf(fml: Formula): PosInExpr
The position of
here()
in the formulafml
.The position of
here()
in the formulafml
. returns
The term or formula position where
here()
occurs infml
.
positionOf("p() & x>2 > here()  x=y^2".asFormula) == PosInExpr(1::0::Nil) positionOf("p() & here() > x=1  x=y^2".asFormula) == PosInExpr(0::1::Nil) positionOf("p() & x>2 > x=1  here()=y^2".asFormula) == PosInExpr(1::1::0::Nil) positionOf("p() & x>2 > x=1  x=here()^2".asFormula) == PosInExpr(1::1::1::0::Nil) positionOf("_ & here() > _  _".asFormula) == PosInExpr(0::1::Nil) positionOf("_ & _ > _  .=here()^2".asFormula) == PosInExpr(1::1::1::0::Nil) positionOf("_ & here() > _".asFormula) == PosInExpr(0::1::Nil)
 Exceptions thrown
IllegalArgumentException
ifhere()
does not occur infml
.
Example: 
def
postCut(cut: Formula): DependentPositionTactic
Prove the given cut formula to hold for the modality at position and turn postcondition into cut>post The operational effect of {a;}*@invariant(f1,f2,f3) is postCut(f1) & postcut(f2) & postCut(f3).
Prove the given cut formula to hold for the modality at position and turn postcondition into cut>post The operational effect of {a;}*@invariant(f1,f2,f3) is postCut(f1) & postcut(f2) & postCut(f3).
cutUseLbl: cutShowLbl: G  [a](C>B), D G  [a]C, D  G  [a]B, D
cutUseLbl: cutShowLbl:  a=2 > [z:=3;][x:=2;](x>1 > [y:=x;]y>1)  [x:=2;]x>1 postCut("x>1".asFormula)(1, 1::1::Nil)  a=2 > [z:=3;][x:=2;][y:=x;]y>1
, cutUseLbl: cutShowLbl:  [x:=2;](x>1 > [y:=x;]y>1)  [x:=2;]x>1 postCut("x>1".asFormula)(1)  [x:=2;][y:=x;]y>1
Examples:  val prop: BelleExpr

def
proveBy(goal: Formula, tactic: BelleExpr): ProvableSig
Prove the new goal by the given tactic, returning the resulting Provable
Prove the new goal by the given tactic, returning the resulting Provable
import StringConverter._ import TactixLibrary._ val proof = TactixLibrary.proveBy("(p()q()>r()) <> (p()>r())&(q()>r())".asFormula, prop)
 See also
TactixLibrary.by(Provable)
Example: 
def
proveBy(goal: Sequent, tactic: BelleExpr): ProvableSig
Prove the new goal by the given tactic, returning the resulting Provable
Prove the new goal by the given tactic, returning the resulting Provable
import StringConverter._ import TactixLibrary._ val proof = TactixLibrary.proveBy(Sequent(IndexedSeq(), IndexedSeq("(p()q()>r()) <> (p()>r())&(q()>r())".asFormula)), prop)
 See also
proveBy()
TactixLibrary.by(Provable)
SequentialInterpreter
Example: 
def
proveBy(goal: ProvableSig, tactic: BelleExpr): ProvableSig
Prove the new goal by the given tactic, returning the resulting Provable
Prove the new goal by the given tactic, returning the resulting Provable
 See also
proveBy()
TactixLibrary.by(Provable)
SequentialInterpreter

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

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

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

val
skip: BelleExpr
nil=skip is a noop tactic that has no effect
nil=skip is a noop tactic that has no effect
 See also

lazy val
solve: DependentPositionTactic
diffSolve: solve a differential equation
[x'=f]p(x)
to\forall t>=0 [x:=solution(t)]p(x)
.diffSolve: solve a differential equation
[x'=f]p(x)
to\forall t>=0 [x:=solution(t)]p(x)
. Similarly,[x'=f(x)&q(x)]p(x)
turns to\forall t>=0 (\forall 0<=s<=t q(solution(s)) > [x:=solution(t)]p(x))
. 
lazy val
solveEnd: DependentPositionTactic
diffSolve with evolution domain check at duration end: solve
[x'=f]p(x)
to\forall t>=0 [x:=solution(t)]p(x)
.diffSolve with evolution domain check at duration end: solve
[x'=f]p(x)
to\forall t>=0 [x:=solution(t)]p(x)
. Similarly,[x'=f(x)&q(x)]p(x)
turns to\forall t>=0 (q(solution(t)) > [x:=solution(t)]p(x))
. 
val
step: DependentPositionTactic
step: one canonical simplifying proof step at the indicated formula/term position (unless @invariant etc needed)

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

def
sublabel(s: String): BelleExpr
Mark the current proof branch and all subbranches s
Mark the current proof branch and all subbranches s
 See also
label()

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

def
tacticChase(tacticIndex: TacticIndex = new DefaultTacticIndex)(restrictTo: AtPosition[_ <: BelleExpr]*): BelleExpr
Exhaustively (depthfirst) apply tactics from the tactic index, restricted to the tactics in
restrictTo
, to chase away. 
lazy val
testb: DependentPositionTactic
testb: [?] simplifies test
[?q;]p
to an implicationq>p
testb: [?] simplifies test
[?q;]p
to an implicationq>p
 Definition Classes
 HilbertCalculus

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

def
throughout(invariant: Formula): DependentPositionTactic
throughout: prove a property of a loop by induction with the given loop invariant (hybrid systems) that holds throughout the steps of the loop body.
throughout: prove a property of a loop by induction with the given loop invariant (hybrid systems) that holds throughout the steps of the loop body. Wipes conditions that contain bound variables of the loop.
use: init: steps: I, G_cnst  p, D_cnst G  I, D I, G_cnst  [a]I, D_cnst I, G_cnst  [b;c;]I, D_cnst I, G_cnst  [d;]I, D_cnst  G  [{a;{b;c;}d}*]p, D

def
toString(): String
 Definition Classes
 AnyRef → Any

def
transform(to: Expression): DependentPositionTactic
Transform an FOL formula or term into the formula/term 'to'.
Transform an FOL formula or term into the formula/term 'to'. A proof why that tranformation is acceptable will be shown on demand. Transforms the FOL formula or term at position 'pos' into the formula/term 'to'. Uses QE to prove the transformation correct.
 to
The transformed formula or term that is desired as the result of this transformation.
*  a<c  a<c  c+0=c transform("c".asFormula)(1, 1::Nil) a<c  a<c+0
, *  a+b<c, b>=0  a+b<c b>=0  a+b<c > a<c  transform("a+b
.asFormula)(1) a+b<c, b>=0  a<c , *  a<b  a<b  a<b > b>a  transform("a.asFormula)(1) a<b  b>a
Examples: 
val
unfoldProgramNormalize: BelleExpr
Follow program structure when normalizing but avoid branching in typical safety problems (splits andR but nothing else).
Follow program structure when normalizing but avoid branching in typical safety problems (splits andR but nothing else). Keeps branching factor of tacticChase restricted to andR.

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

def
useLemma(lemma: Lemma, adapt: Option[BelleExpr]): BelleExpr
useLemma(lemma, tactic) applies the
lemma
, optionally adapting the lemma formula to the current subgoal using the tacticadapt
.useLemma(lemma, tactic) applies the
lemma
, optionally adapting the lemma formula to the current subgoal using the tacticadapt
. Literal lemma application ifadapt
is None. 
def
useLemma(lemmaName: String, adapt: Option[BelleExpr]): BelleExpr
useLemma(lemmaName, tactic) applies the lemma identified by
lemmaName
, optionally adapting the lemma formula to the current subgoal using the tacticadapt
.useLemma(lemmaName, tactic) applies the lemma identified by
lemmaName
, optionally adapting the lemma formula to the current subgoal using the tacticadapt
. Literal lemma application ifadapt
is None. 
def
useLemmaAt(lemmaName: String, key: Option[PosInExpr]): DependentPositionWithAppliedInputTactic
Applies the lemma by matching
key
in the lemma with the tactic position. 
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( ... )

def
withAbstraction(t: AtPosition[_ <: BelleExpr]): DependentPositionTactic
'position' tactic t with universal abstraction at the same position afterwards
'position' tactic t with universal abstraction at the same position afterwards
 See also
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.