trait HilbertCalculus extends UnifyUSCalculus
Hilbert Calculus for differential dynamic logic.
Provides the axioms and axiomatic proof rules from Figure 2 and Figure 3 in: Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
- See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.
Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981
Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980
Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. IEEE 2012
Andre Platzer. The complete proof theory of hybrid systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 541-550. IEEE 2012
HilbertCalculus.stepAt()
HilbertCalculus.derive()
edu.cmu.cs.ls.keymaerax.core.AxiomBase
- Alphabetic
- By Inheritance
- HilbertCalculus
- UnifyUSCalculus
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
type
ForwardPositionTactic = (Position) ⇒ ForwardTactic
Forward-style position tactic mapping positions and provables to provables that follow from it.
Forward-style position tactic mapping positions and provables to provables that follow from it.
- Definition Classes
- UnifyUSCalculus
-
type
ForwardTactic = (ProvableSig) ⇒ ProvableSig
Forward-style tactic mapping provables to provables that follow from it.
Forward-style tactic mapping provables to provables that follow from it.
- Definition Classes
- UnifyUSCalculus
-
type
Subst = RenUSubst
The (generalized) substitutions used for unification
The (generalized) substitutions used for unification
- Definition Classes
- UnifyUSCalculus
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
CE(C: Context[Formula]): ForwardTactic
CE(C) will wrap any equivalence
left<->right
or equalityleft=right
fact it gets within context C.CE(C) will wrap any equivalence
left<->right
or equalityleft=right
fact it gets within context C. Uses CE or CQ as needed.p(x) <-> q(x) --------------------- CE C{p(x)} <-> C{q(x)}
f(x) = g(x) --------------------- CQ+CE c(f(x)) <-> c(g(x))
- Definition Classes
- UnifyUSCalculus
- To do
likewise for Context[Term] using CT instead.
- See also
CE(PosInExpr
CEat(Provable)
CMon(Context)
-
def
CE(inEqPos: PosInExpr): InputTactic
CE(pos) at the indicated position within an equivalence reduces contextual equivalence
C{left}<->C{right}
to argument equivalenceleft<->right
.CE(pos) at the indicated position within an equivalence reduces contextual equivalence
C{left}<->C{right}
to argument equivalenceleft<->right
.p(x) <-> q(x) --------------------- CE C{p(x)} <-> C{q(x)}
Part of the differential dynamic logic Hilbert calculus.
- inEqPos
the position *within* the two sides of the equivalence at which the context DotFormula occurs.
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$88 , x$87 , x$89 , x$85 , x$86 , x$90 , x$91 , x$92 , x$93 , x$94 , x$95 , x$96 )
- See also
UnifyUSCalculus.CE(Context)
UnifyUSCalculus.CQ(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)
UnifyUSCalculus.CEat(Provable)
Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981
-
def
CEat(fact: ProvableSig, C: Context[Formula]): DependentPositionTactic
CEat(fact,C) uses the equivalence
left<->right
or equalityleft=right
or implicationleft->right
fact for congruence reasoning in the given context C at the indicated position to replaceright
byleft
in that context (literally, no substitution).CEat(fact,C) uses the equivalence
left<->right
or equalityleft=right
or implicationleft->right
fact for congruence reasoning in the given context C at the indicated position to replaceright
byleft
in that context (literally, no substitution).- Definition Classes
- UnifyUSCalculus
CE(fact, Context("⎵".asFormula))
is equivalent toCE(fact)
. , CE(fact, Context("x>0&⎵".asFormula))(p)
is equivalent toCE(fact)(p+PosInExpr(1::Nil))
. Except that the former has the shapex>0&⎵
for the context starting from positionp
.- See also
UnifyUSCalculus.CEat(Provable)
useAtImpl()
CE(Context)
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CQ(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)
Examples: -
def
CEat(fact: ProvableSig, key: PosInExpr): BuiltInPositionTactic
CEat replacing
key
with the other expression in the equality/equivalence.CEat replacing
key
with the other expression in the equality/equivalence. @see CEat(ProvableSig)- Definition Classes
- UnifyUSCalculus
-
def
CEat(fact: ProvableSig): BuiltInPositionTactic
CEat(fact) uses the equivalence
left<->right
or equalityleft=right
or implicationleft->right
fact for congruence reasoning at the indicated position to replaceright
byleft
at indicated position (literally, no substitution).CEat(fact) uses the equivalence
left<->right
or equalityleft=right
or implicationleft->right
fact for congruence reasoning at the indicated position to replaceright
byleft
at indicated position (literally, no substitution). Efficient unification-free 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.CEat(Provable,Context)
useAtImpl()
CE(Context)
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CQ(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)
Example: -
def
CEimp(inEqPos: PosInExpr): InputTactic
CEimply(pos) at the indicated position within an equivalence reduces contextual implication
C{left}->C{right}
to argument equivalenceleft<->right
.CEimply(pos) at the indicated position within an equivalence reduces contextual implication
C{left}->C{right}
to argument equivalenceleft<->right
.p(x) <-> q(x) --------------------- CE C{p(x)} -> C{q(x)}
Part of the differential dynamic logic Hilbert calculus.
- inEqPos
the position *within* the two sides of the equivalence at which the context DotFormula occurs.
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$99 , x$100 , x$101 , x$97 , x$98 , x$102 , x$103 , x$104 , x$105 , x$106 , x$107 , x$108 )
- See also
UnifyUSCalculus.CE(Context)
Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981
-
def
CErevimp(inEqPos: PosInExpr): InputTactic
CErevimply(pos) at the indicated position within an equivalence reduces contextual implication
C{left}->C{right}
to argument equivalenceleft<->right
.CErevimply(pos) at the indicated position within an equivalence reduces contextual implication
C{left}->C{right}
to argument equivalenceleft<->right
.q(x) <-> p(x) --------------------- CE C{p(x)} -> C{q(x)}
Part of the differential dynamic logic Hilbert calculus.
- inEqPos
the position *within* the two sides of the equivalence at which the context DotFormula occurs.
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$111 , x$112 , x$113 , x$109 , x$110 , x$114 , x$115 , x$116 , x$117 , x$118 , x$119 , x$120 )
- See also
UnifyUSCalculus.CE(Context)
Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981
-
def
CMon(C: Context[Formula]): ForwardTactic
CMon(C) will wrap any implication
left->right
fact it gets within a (positive or negative) context C by monotonicity.CMon(C) will wrap any implication
left->right
fact it gets within a (positive or negative) context C by monotonicity.k |- o ------------ CMon if C{⎵} of positive polarity C{k} |- C{o}
- Definition Classes
- UnifyUSCalculus
- Note
The direction in the conclusion switches for negative polarity C{⎵}
- See also
UnifyUSCalculus.CMon(PosInExpr)
CE(Context)
-
def
CMon: BuiltInRightTactic
Convenience CMon first hiding other context.
Convenience CMon first hiding other context.
|- o -> k ------------------------- for positive C{.} G |- C{o} -> C{k}, D
|- k -> o ------------------------- for negative C{.} G |- C{o} -> C{k}, D
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$135 , x$136 , x$137 , x$133 , x$134 , x$138 , x$139 , x$140 , x$141 , x$142 , x$143 , x$144 )
- See also
CMon()
-
def
CMon(inEqPos: PosInExpr): InputTactic
CMon(pos) at the indicated position within an implication reduces contextual implication
C{o}->C{k}
to argument implicationo->k
for positive C.CMon(pos) at the indicated position within an implication reduces contextual implication
C{o}->C{k}
to argument implicationo->k
for positive C. Contextual monotonicity proof rule.|- o -> k ------------------------- for positive C{.} |- C{o} -> C{k}
|- k -> o ------------------------- for negative C{.} |- C{o} -> C{k}
- inEqPos
the position *within* the two sides C{.} of the implication at which the context DotFormula happens.
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$124 , x$123 , x$125 , x$121 , x$122 , x$126 , x$127 , x$128 , x$129 , x$130 , x$131 , x$132 )
- See also
UnifyUSCalculus.CQ(PosInExpr)
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CMon(Context)
UnifyUSCalculus.CEat())
-
def
CQ(inEqPos: PosInExpr): InputTactic
CQ(pos) at the indicated position within an equivalence reduces contextual equivalence
p(left)<->p(right)
to argument equalityleft=right
.CQ(pos) at the indicated position within an equivalence reduces contextual equivalence
p(left)<->p(right)
to argument equalityleft=right
. This tactic will use CEat() under the hood as needed.f(x) = g(x) --------------------- CQ c(f(x)) <-> c(g(x))
- inEqPos
the position *within* the two sides of the equivalence at which the context DotTerm happens.
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$51 , x$52 , x$53 , x$49 , x$50 , x$54 , x$55 , x$56 , x$57 , x$58 , x$59 , x$60 )
- See also
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)
-
def
CQimp(inEqPos: PosInExpr): InputTactic
CQimply(pos) at the indicated position within an equivalence reduces contextual implication
p(left)->p(right)
to argument equalityleft=right
.CQimply(pos) at the indicated position within an equivalence reduces contextual implication
p(left)->p(right)
to argument equalityleft=right
. This tactic will use CEat() under the hood as needed.f(x) = g(x) --------------------- CQ c(f(x)) -> c(g(x))
- inEqPos
the position *within* the two sides of the equivalence at which the context DotTerm happens.
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$63 , x$64 , x$65 , x$61 , x$62 , x$66 , x$67 , x$68 , x$69 , x$70 , x$71 , x$72 )
- See also
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)
-
def
CQrevimp(inEqPos: PosInExpr): InputTactic
CQrevimp(pos) at the indicated position within an equivalence reduces contextual implication
p(left)->p(right)
to argument equalityleft=right
.CQrevimp(pos) at the indicated position within an equivalence reduces contextual implication
p(left)->p(right)
to argument equalityleft=right
. This tactic will use CEat() under the hood as needed.g(x) = f(x) --------------------- CQ c(f(x)) -> c(g(x))
- inEqPos
the position *within* the two sides of the equivalence at which the context DotTerm happens.
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$75 , x$76 , x$77 , x$73 , x$74 , x$78 , x$79 , x$80 , x$81 , x$82 , x$83 , x$84 )
- See also
UnifyUSCalculus.CE(PosInExpr)
UnifyUSCalculus.CMon(PosInExpr)
-
def
DC(invariant: Formula): DependentPositionWithAppliedInputTactic
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)
.Use: Show: G |- [x'=f(x)&Q&R]P, D G |- [x'=f(x)&Q]R, D ---------------------------------------------- DC(R) G |- [x'=f(x)&Q]P, D
Use: Show: G |- A->[x'=f(x)&Q&R]P, D G |- A->[x'=f(x)&Q]R, D ---------------------------------------------- dC(R) G |- A->[x'=f(x)&Q]P, D
- Annotations
- @Tactic( x$124 , x$125 , x$126 , x$127 , x$121 , x$128 , x$129 , x$130 , x$131 , x$123 , x$122 , x$132 )
- See also
DifferentialEquationCalculus.dC()
-
def
DCd(invariant: Formula): DependentPositionWithAppliedInputTactic
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)
.- Annotations
- @Tactic( x$136 , x$137 , x$138 , x$139 , x$133 , x$140 , x$141 , x$142 , x$143 , x$135 , x$134 , x$144 )
-
lazy val
DE: DependentPositionTactic
DE: Differential Effect exposes the effect of a differential equation
[x'=f(x)]p(x,x')
on its differential symbols as[x'=f(x)][x':=f(x)]p(x,x')
with its differential assignmentx':=f(x)
.DE: Differential Effect exposes the effect of a differential equation
[x'=f(x)]p(x,x')
on its differential symbols as[x'=f(x)][x':=f(x)]p(x,x')
with its differential assignmentx':=f(x)
.G |- [{x'=f(||)&H(||)}][x':=f(||);]p(||), D ------------------------------------------- G |- [{x'=f(||)&H(||)}]p(||), D
|- [{x'=1}][x':=1;]x>0 -----------------------DE(1) |- [{x'=1}]x>0
, |- [{x'=1, y'=x & x>0}][y':=x;][x':=1;]x>0 -------------------------------------------DE(1) |- [{x'=1, y'=x & x>0}]x>0
Examples: -
lazy val
DI: BuiltInPositionTactic
DI: Differential Invariants are used for proving a formula to be an invariant of a differential equation.
DI: Differential Invariants are used for proving a formula to be an invariant of a differential equation.
[x'=f(x)&q(x)]p(x)
reduces toq(x) -> p(x) & [x'=f(x)]p(x)'
.- See also
DifferentialEquationCalculus.dI()
-
lazy val
DS: BuiltInPositionTactic
DS: Differential Solution solves a simple differential equation
[x'=c&q(x)]p(x)
by reduction to\forall t>=0 ((\forall 0<=s<=t q(x+c()*s) -> [x:=x+c()*t;]p(x))
-
lazy val
DW: BuiltInPositionTactic
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))
.G |- [x'=f(x)&Q](Q->P), D ------------------------- DW(R) G |- [x'=f(x)&Q]P, D
- See also
DifferentialEquationCalculus.dW()
-
lazy val
DWd: BuiltInPositionTactic
DWd: Diamond Differential Weakening to use evolution domain constraint
<{x'=f(x)&q(x)}>p(x)
reduces to<{x'=f(x)&q(x)}>(q(x)&p(x))
-
lazy val
Dassignb: BuiltInPositionTactic
Dassignb: [':=] Substitute a differential assignment
[x':=f]p(x')
top(f)
-
val
G: DependentPositionTactic
G: Gödel generalization rule reduces a proof of
Γ |- [a]p(x), Δ
to proving the postcondition|- p(x)
in isolation. -
lazy val
K: BuiltInPositionTactic
K: modal modus ponens (hybrid systems)
-
def
US(fact: ProvableSig): BuiltInTactic
US(fact) uses a suitable uniform substitution to reduce the proof to the proof of
fact
.US(fact) uses a suitable uniform substitution to reduce the proof to the proof of
fact
. Unifies the current sequent withfact.conclusion
. Use that unifier as a uniform substitution to instantiatefact
with.fact: g |- d --------- US where G=s(g) and D=s(d) where s=unify(fact.conclusion, G|-D) 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
US(subst) uses a uniform substitution of rules to transform an entire provable.
US(subst) uses a uniform substitution of rules to transform an entire provable.
G1 |- D1 ... Gn |- Dn s(G1) |- s(D1) ... s(Gn) |- s(Dn) ----------------------- => ----------------------------------- (USR) G |- D s(G) |- s(D)
- subst
The uniform substitution
s
(of no free variables) to be used on the premises and conclusion of the provable.
- Definition Classes
- UnifyUSCalculus
- See also
edu.cmu.cs.ls.keymaerax.core.Provable.apply(USubst)
ProvableInfo)
-
def
US(subst: USubst, fact: ProvableSig): BuiltInTactic
US(subst, fact) reduces the present proof to a proof of
fact
, whose uniform substitution instance undersubst
the current goal is.US(subst, fact) reduces the present proof to a proof of
fact
, whose uniform substitution instance undersubst
the current goal is.s(g1) |- s(d1) ... s(gn) |- s(dn) g1 |- d1 ... gn |- dn --------------------------------- if ----------------------- fact G |- D g |- d where G=s(g) and D=s(d)
- subst
the substitution
s
that instantiates factg |- d
to the present goalG |- D
.- fact
the fact
g |- d
to reduce the proof to. Facts do not have to be proved yet.
- Definition Classes
- UnifyUSCalculus
- See also
edu.cmu.cs.ls.keymaerax.core.Provable.apply(USubst)
ProvableInfo)
-
def
US(subst: USubst, fact: ProvableInfo): BuiltInTactic
US(subst, fact) reduces the proof to the given fact, whose uniform substitution instance under
subst
the current goal is.US(subst, fact) reduces the proof to the given fact, whose uniform substitution instance under
subst
the current goal is. Whenfact
is an axiom:* * --------- if -------- fact G |- D g |- d where G=s(g) and D=s(d)
When
fact
is an axiomatic rule:s(g1) |- s(d1) ... s(gn) |- s(dn) g1 |- d1 ... gn |- dn --------------------------------- if ----------------------- fact G |- D g |- d where G=s(g) and D=s(d)
- subst
the substitution
s
that instantiates factg |- d
to the present goalG |- D
.- fact
the provable for the axiom
g |- d
to reduce the proof to (accordingly for axiomatic rules).
- Definition Classes
- UnifyUSCalculus
- See also
US(USubst,ProvableSig)
-
def
USX(S: List[SubstitutionPair]): InputTactic
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$37 , x$38 , x$41 , x$40 , x$39 , x$42 , x$43 , x$44 , x$45 , x$46 , x$47 , x$48 )
-
lazy val
V: BuiltInPositionTactic
V: vacuous box
[a]p()
will be discarded and replaced byp()
provided programa
does not change values of postconditionp()
.V: vacuous box
[a]p()
will be discarded and replaced byp()
provided programa
does not change values of postconditionp()
.- Note
Unsound for hybrid games
-
lazy val
VK: BuiltInPositionTactic
VK: vacuous box
[a]p()
will be discarded and replaced byp()
provided programa
does not change values of postconditionp()
and provided[a]true
proves, e.g., sincea
is a hybrid system. -
lazy val
allDist: BuiltInPositionTactic
allDist: distribute
\forall x p(x) -> \forall x q(x)
by replacing it with\forall x (p(x)->q(x))
.allDist: distribute
\forall x p(x) -> \forall x q(x)
by replacing it with\forall x (p(x)->q(x))
.- See also
-
lazy val
allDistElim: BuiltInPositionTactic
allDistElim: distribute
\forall x P -> \forall x Q
by replacing it with\forall x (P->Q)
. -
lazy val
allV: BuiltInPositionTactic
allV: vacuous
\forall x p()
will be discarded and replaced by p() provided x does not occur in p(). -
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
lazy val
assignb: BuiltInPositionTactic
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 top-level in the succedent; they remain unhandled in the antecedent and in non-top-level context.- Annotations
- @Tactic( x$1 , x$4 , x$5 , x$6 , x$3 , x$7 , x$8 , x$9 , x$10 , x$2 , x$11 , x$12 )
|- 1>0 --------------------assignb(1) |- [x:=1;]x>0
, 1>0 |- --------------------assignb(-1) [x:=1;]x>0 |-
, x_0=1 |- [{x_0:=x_0+1;}*]x_0>0 ----------------------------------assignb(1) |- [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 |-
, |- [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
- See also
DLBySubst.assignEquality
Examples: -
lazy val
assignbDual: BuiltInPositionTactic
- Annotations
- @Tactic( x$109 , x$111 , x$112 , x$113 , x$110 , x$114 , x$115 , x$116 , x$117 , x$118 , x$119 , x$120 )
-
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- Annotations
- @Tactic( x$73 , x$76 , x$77 , x$78 , x$75 , x$79 , x$80 , x$81 , x$82 , x$74 , x$83 , x$84 )
- lazy val assigndDual: BuiltInPositionTactic
-
def
boundRename(what: Variable, repl: Variable): BuiltInPositionTactic
boundRename(what,repl) renames
what
torepl
at the indicated position (or vice versa).boundRename(what,repl) renames
what
torepl
at the indicated position (or vice versa).- Definition Classes
- UnifyUSCalculus
- See also
-
lazy val
box: BuiltInPositionTactic
box: [.] to reduce double-negated diamond
!⟨a⟩!p(x)
to a box[a]p(x)
. -
lazy val
boxAnd: BuiltInPositionTactic
boxAnd: splits
[a](p&q)
into[a]p & [a]q
-
lazy val
boxImpliesAnd: BuiltInPositionTactic
boxImpliesAnd: splits
[a](p->q&r)
into[a](p->q) & [a](p->r)
-
lazy val
boxTrue: BuiltInPositionTactic
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.- Annotations
- @Tactic( x$145 , x$148 , x$149 , x$150 , x$146 , x$151 , x$152 , x$147 , x$153 , x$154 , x$155 , x$156 )
-
lazy val
boxd: BuiltInPositionTactic
- Annotations
- @Tactic( x$97 , x$99 , x$100 , x$101 , x$98 , x$102 , x$103 , x$104 , x$105 , x$106 , x$107 , x$108 )
-
def
by(lemma: Lemma, subst: Subst): BelleExpr
by(name,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.
by(name,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.
- Definition Classes
- UnifyUSCalculus
-
def
by(lemma: Lemma, subst: USubst): BelleExpr
- Definition Classes
- UnifyUSCalculus
-
def
by(pi: ProvableInfo, subst: Subst): BelleExpr
- Definition Classes
- UnifyUSCalculus
-
def
by(pi: ProvableInfo, subst: USubst): BelleExpr
by(pi,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.
by(pi,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.
s(a) |- s(b) a |- b ------------- rule(---------) if s(g)=G and s(d)=D G |- D g |- d
- pi
the provable to use to prove the sequent
- subst
what substitution
s
to use for instantiating the factpi
.
- Definition Classes
- UnifyUSCalculus
- See also
byUS()
-
def
by(lemma: Lemma): BelleExpr
- Definition Classes
- UnifyUSCalculus
-
def
by(pi: ProvableInfo): BelleExpr
by(pi) uses the given provable with its information literally to continue or close the proof (if it fits to what has been proved).
by(pi) uses the given provable with its information literally to continue or close the proof (if it fits to what has been proved).
- pi
the information for the Provable to use, e.g., from Ax.
- Definition Classes
- UnifyUSCalculus
-
def
byUS(pi: ProvableInfo, inst: (Subst) ⇒ Subst): BelleExpr
rule(pi,inst) uses the given axiom or axiomatic rule to prove the sequent.
rule(pi,inst) uses the given axiom or axiomatic rule to prove the sequent. Unifies the fact's conclusion with the current sequent and proceed to the instantiated premise of
fact
.s(a) |- s(b) a |- b ------------- rule(---------) if s(g)=G and s(d)=D G |- D g |- d
The behavior of rule(Provable) is essentially the same as that of by(Provable) except that the former prefetches the uniform substitution instance during tactics applicability checking.
- pi
the provable info for the fact to use to prove the sequent
- inst
Transformation for instantiating additional unmatched symbols that do not occur in the conclusion. Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also modify the unifier if other cases than the most-general unifier are preferred.
- Definition Classes
- UnifyUSCalculus
- See also
byUS()
by()
-
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): BuiltInTactic
byUS(pi) proves by a uniform substitution instance of provable (information), obtained by unification with the current goal.
byUS(pi) proves by a uniform substitution instance of provable (information), obtained by unification with the current goal. Like by(ProvableInfo,USubst) except that the required substitution is automatically obtained by unification.
- Definition Classes
- UnifyUSCalculus
- See also
UnifyUSCalculus.US()
-
def
byUS(pi: ProvableInfo): BelleExpr
byUS(pi) proves by a uniform substitution instance of provable (information) or axiom or axiomatic rule, obtained by unification with the current goal.
byUS(pi) proves by a uniform substitution instance of provable (information) or axiom or axiomatic rule, obtained by unification with the current goal. Like by(ProvableInfo,USubst) except that the required substitution is automatically obtained by unification.
- Definition Classes
- UnifyUSCalculus
- See also
UnifyUSCalculus.US()
-
def
chase(keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst = ax=>us=>us, index: (ProvableInfo) ⇒ (PosInExpr, List[PosInExpr]) = AxIndex.axiomIndex): BuiltInPositionTactic
chase: Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices.
chase: Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices.
Chase the expression at the indicated position forward (Hilbert computation constructing the answer by proof). Follows canonical axioms toward all their recursors while there is an applicable simplifier axiom according to
keys
.- keys
maps expressions to a list of axiom names to be used for those expressions. First returned axioms will be favored (if applicable) over further axioms. Defaults to AxIndex.axiomFor().
- modifier
will be notified after successful uses of axiom at a position with the result of the use. The result of modifier(ax,pos)(step) will be used instead of step for each step of the chase. Defaults to identity transformation, i.e., no modification in found match.
- inst
Transformation for instantiating additional unmatched symbols that do not occur when using the given axiom _1. Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the most-general unifier are preferred.
- index
Provides recursors to continue chase after applying an axiom from
keys
. Defaults to AxIndex.axiomIndex.
- Definition Classes
- UnifyUSCalculus
When applied at 1::Nil, turns [{x'=22}](2*x+x*y>=5)' into [{x'=22}]2*x'+(x'*y+x*y')>=0
, When applied at Nil, turns [?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into ((x>0->x+1>=1) & (x=0->1>=1))
, When applied at 1::Nil, turns [{x'=22}][?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into [{x'=22}]((x>0->x+1>=1) & (x=0->1>=1))
- To do
also implement a backwards chase in tableaux/sequent style based on useAt instead of useFor
- Note
Chase is search-free and, thus, quite efficient. It directly follows the axiom index information to compute follow-up positions for the chase.
- See also
chaseFor()
Examples: -
def
chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic): BuiltInPositionTactic
- Definition Classes
- UnifyUSCalculus
-
def
chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo]): BuiltInPositionTactic
- Definition Classes
- UnifyUSCalculus
-
def
chase(breadth: Int, giveUp: Int): BuiltInPositionTactic
Chase with bounded breadth and giveUp to stop.
Chase with bounded breadth and giveUp to stop.
- breadth
how many alternative axioms to pursue locally, using the first applicable one. Equivalent to pruning keys so that all lists longer than giveUp are replaced by Nil, and then all lists are truncated beyond breadth.
- giveUp
how many alternatives are too much so that the chase stops without trying any for applicability. Equivalent to pruning keys so that all lists longer than giveUp are replaced by Nil.
- Definition Classes
- UnifyUSCalculus
-
val
chase: BuiltInPositionTactic
Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices.
Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices. Unlike TactixLibrary.chaseAt will not branch or use propositional rules, merely transform the chosen formula in place.
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$2 , x$3 , x$1 , x$4 , x$5 , x$6 , x$7 , x$8 , x$9 , x$10 , x$11 , x$12 )
-
def
chaseCustom(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): BuiltInPositionTactic
chaseCustom: Unrestricted form of chase where AxiomIndex is not built in, i.e.
chaseCustom: Unrestricted form of chase where AxiomIndex is not built in, i.e. it takes keys of the form Expression => List[(Provable,PosInExpr, List[PosInExpr])] This allows customized rewriting using provables derived at runtime
- Definition Classes
- UnifyUSCalculus
-
def
chaseCustomFor(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): ForwardPositionTactic
- Definition Classes
- UnifyUSCalculus
-
def
chaseFor(keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst = ax=>us=>us, index: (ProvableInfo) ⇒ (PosInExpr, List[PosInExpr])): ForwardPositionTactic
chaseFor: Chases the expression of Provables at given positions forward until it is chased away or can't be chased further without critical choices.
chaseFor: Chases the expression of Provables at given positions forward until it is chased away or can't be chased further without critical choices.
Chase the expression at the indicated position forward (Hilbert computation constructing the answer by proof). Follows canonical axioms toward all their recursors while there is an applicable simplifier axiom according to
keys
.- keys
maps expressions to a list of axioms/tactics to be used for those expressions. The first applicable axiom/tactic will be chosen. Defaults to AxIndex.axiomIndex.
- modifier
will be notified after successful uses of axiom at a position with the result of the use. The result of modifier(ax,pos)(step) will be used instead of step for each step of the chase. Defaults to identity transformation, i.e., no modification in found match.
- inst
Transformation for instantiating additional unmatched symbols that do not occur when using the given axiom. Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the most-general unifier are preferred.
- index
The key and recursor information determining (as in AxiomInfo)
._1
which subexpression of the ProvableInfo to match against.._2
which resulting recursors to continue chasing after in the resulting expression. Defaults to AxIndex.axiomIndex.
- Definition Classes
- UnifyUSCalculus
When applied at 1::Nil, turns [{x'=22}](2*x+x*y>=5)' into [{x'=22}]2*x'+(x'*y+x*y')>=0
, When applied at Nil, turns [?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into ((x>0->x+1>=1) & (x=0->1>=1))
, When applied at 1::Nil, turns [{x'=22}][?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into [{x'=22}]((x>0->x+1>=1) & (x=0->1>=1))
- Note
Chase is search-free and, thus, quite efficient. It directly follows the axiom index information to compute follow-up positions for the chase.
- See also
chase()
Examples: -
def
chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst, index: (ProvableInfo) ⇒ (PosInExpr, List[PosInExpr])): ForwardPositionTactic
- Definition Classes
- UnifyUSCalculus
-
def
chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst): ForwardPositionTactic
- Definition Classes
- UnifyUSCalculus
-
def
chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic): ForwardPositionTactic
- Definition Classes
- UnifyUSCalculus
-
def
chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst, index: (ProvableInfo) ⇒ (PosInExpr, List[PosInExpr])): BuiltInPositionTactic
- Definition Classes
- UnifyUSCalculus
-
def
chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst): BuiltInPositionTactic
- Definition Classes
- UnifyUSCalculus
-
def
chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst): BuiltInPositionTactic
- Definition Classes
- UnifyUSCalculus
-
lazy val
choiceb: BuiltInPositionTactic
choiceb: [++] handles both cases of a nondeterministic choice
[a++b]p(x)
separately[a]p(x) & [b]p(x)
-
lazy val
choiced: BuiltInPositionTactic
choiced: <++> handles both cases of a nondeterministic choice
⟨a++b⟩p(x)
separately⟨a⟩p(x) | ⟨b⟩p(x)
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
def
commuteEquivFR: ForwardPositionTactic
commuteEquivFR commutes the equivalence at the given position (for forward tactics).
commuteEquivFR commutes the equivalence at the given position (for forward tactics).
- Definition Classes
- UnifyUSCalculus
-
lazy val
composeb: BuiltInPositionTactic
composeb: [;] handle both parts of a sequential composition
[a;b]p(x)
one at a time[a][b]p(x)
-
lazy val
composed: BuiltInPositionTactic
composed: <;> handle both parts of a sequential composition
⟨a;b⟩p(x)
one at a time⟨a⟩⟨b⟩p(x)
-
def
cutAt(repl: Expression): DependentPositionWithAppliedInputTactic
cutAt(repl) cuts left/right to replace the expression at the indicated position in its context C{.} by
repl
.cutAt(repl) cuts left/right to replace the expression at the indicated position in its context C{.} by
repl
.G |- C{repl}, D G |- C{repl}->C{c}, D --------------------------------------- cutAt(repl) G |- C{c}, D
C{repl}, G |- D G |- D, C{c}->C{repl} --------------------------------------- cutAt(repl) C{c}, G |- D
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$147 , x$148 , x$149 , x$145 , x$146 , x$150 , x$151 , x$152 , x$153 , x$154 , x$155 , x$156 )
- See also
UnifyUSCalculus.CEat(Provable)
-
val
deepChase: BuiltInPositionTactic
Chases the expression at the indicated position forward.
Chases the expression at the indicated position forward. Unlike chase descends into formulas and terms exhaustively.
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( x$14 , x$15 , x$13 , x$16 , x$17 , x$18 , x$19 , x$20 , x$21 , x$22 , x$23 , x$24 )
-
lazy val
derive: BuiltInPositionTactic
Derive the differential expression at the indicated position (Hilbert computation deriving the answer by proof) to get rid of the differential operators.
Derive the differential expression at the indicated position (Hilbert computation deriving the answer by proof) to get rid of the differential operators.
- Annotations
- @Tactic( x$49 , x$51 , x$52 , x$53 , x$54 , x$55 , x$56 , x$57 , x$58 , x$50 , x$59 , x$60 )
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: BuiltInPositionTactic
diamond: <.> reduce double-negated box
![a]!p(x)
to a diamond⟨a⟩p(x)
. -
lazy val
diamondOr: BuiltInPositionTactic
diamondOr: splits
⟨a⟩(p|q)
into⟨a⟩p | ⟨a⟩q
-
lazy val
diamondd: BuiltInPositionTactic
- Annotations
- @Tactic( x$61 , x$63 , x$64 , x$65 , x$62 , x$66 , x$67 , x$68 , x$69 , x$70 , x$71 , x$72 )
-
lazy val
dualb: BuiltInPositionTactic
dualb: [d] handle dual game
[{a}d]p(x)
by![a]!p(x)
-
lazy val
duald: BuiltInPositionTactic
duald:
<d>
handle dual game⟨{a}d⟩p(x)
by!⟨a⟩!p(x)
-
def
either(left: ForwardTactic, right: ForwardTactic): ForwardTactic
either(left,right) runs
left
if successful andright
otherwise (for forward tactics).either(left,right) runs
left
if successful andright
otherwise (for forward tactics).- Definition Classes
- UnifyUSCalculus
-
def
eitherP(left: ForwardPositionTactic, right: ForwardPositionTactic): ForwardPositionTactic
eitherP(left,right) runs
left
if successful andright
otherwise (for forward tactics).eitherP(left,right) runs
left
if successful andright
otherwise (for forward tactics).- Definition Classes
- UnifyUSCalculus
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
lazy val
existsE: BuiltInPositionTactic
existsE: show
\exists x P
by showing that it follows fromP
. -
lazy val
existsV: BuiltInPositionTactic
existsV: vacuous
\exists x p()
will be discarded and replaced by p() provided x does not occur in p(). -
val
fail: BuiltInTactic
fail is a tactic that always fails as being inapplicable
fail is a tactic that always fails as being inapplicable
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
- See also
-
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
iden: ForwardTactic
identity tactic skip that does not no anything (for forward tactics).
identity tactic skip that does not no anything (for forward tactics).
- Definition Classes
- UnifyUSCalculus
-
def
ifThenElse(cond: (ProvableSig) ⇒ Boolean, thenT: ForwardTactic, elseT: ForwardTactic): ForwardTactic
ifThenElse(cond,thenT,elseT) runs
thenT
ifcond
holds andelseT
otherwise (for forward tactics).ifThenElse(cond,thenT,elseT) runs
thenT
ifcond
holds andelseT
otherwise (for forward tactics).- Definition Classes
- UnifyUSCalculus
-
def
ifThenElseP(cond: (Position) ⇒ (ProvableSig) ⇒ Boolean, thenT: ForwardPositionTactic, elseT: ForwardPositionTactic): ForwardPositionTactic
ifThenElseP(cond,thenT,elseT) runs
thenT
ifcond
holds andelseT
otherwise (for forward tactics).ifThenElseP(cond,thenT,elseT) runs
thenT
ifcond
holds andelseT
otherwise (for forward tactics).- Definition Classes
- UnifyUSCalculus
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
lazy val
iterateb: BuiltInPositionTactic
iterateb: [*] prove a property of a loop
[{a}*]p(x)
by unrolling it oncep(x) & [a][{a}*]p(x)
-
lazy val
iterated: BuiltInPositionTactic
iterated: <*> prove a property of a loop
⟨{a}*⟩p(x)
by unrolling it oncep(x) | ⟨a⟩⟨{a}*⟩p(x)
-
def
let(abbr: Expression, value: Expression, inner: BelleExpr): BelleExpr
Let(abbr, value, inner) alias
let abbr=value in inner
abbreviatesvalue
byabbr
in the provable and proceeds with an internal proof by tacticinner
, resuming to the outer proof by a uniform substitution ofvalue
forabbr
of the resulting provable.Let(abbr, value, inner) alias
let abbr=value in inner
abbreviatesvalue
byabbr
in the provable and proceeds with an internal proof by tacticinner
, resuming to the outer proof by a uniform substitution ofvalue
forabbr
of the resulting provable.- Definition Classes
- UnifyUSCalculus
-
lazy val
monall: BuiltInTactic
allG: all generalization rule reduces a proof of
\forall x p(x) |- \forall x q(x)
to provingp(x) |- q(x)
in isolation.allG: all generalization rule reduces a proof of
\forall x p(x) |- \forall x q(x)
to provingp(x) |- q(x)
in isolation.p(x) |- q(x) --------------------------------- \forall x p(x) |- \forall x q(x)
- Annotations
- @Tactic( x$87 , x$88 , x$89 , x$85 , x$86 , x$90 , x$91 , x$92 , x$93 , x$94 , x$95 , x$96 )
- See also
UnifyUSCalculus.CMon()
-
lazy val
monb: BuiltInTactic
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)
.p(x) |- q(x) ------------------- M[.] [a]p(x) |- [a]q(x)
- Annotations
- @Tactic( x$27 , x$28 , x$29 , x$25 , x$26 , x$30 , x$31 , x$32 , x$33 , x$34 , x$35 , x$36 )
- See also
UnifyUSCalculus.CMon()
-
lazy val
mond: BuiltInTactic
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)
.p(x) |- q(x) ------------------- M ⟨a⟩p(x) |- ⟨a⟩q(x)
- Annotations
- @Tactic( x$15 , x$16 , x$17 , x$13 , x$14 , x$18 , x$19 , x$20 , x$21 , x$22 , x$23 , x$24 )
- See also
UnifyUSCalculus.CMon()
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
val
nil: BuiltInTactic
nil=skip is a no-op tactic that has no effect
nil=skip is a no-op tactic that has no effect
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
lazy val
randomb: BuiltInPositionTactic
randomb: [:*] simplify nondeterministic assignment
[x:=*;]p(x)
to a universal quantifier\forall x p(x)
-
lazy val
randomd: BuiltInPositionTactic
randomd: <:*> simplify nondeterministic assignment
<x:=*;>p(x)
to an existential quantifier\exists x p(x)
-
def
seqCompose(first: ForwardTactic, second: ForwardTactic): ForwardTactic
seqCompose(first,second) runs
first
followed bysecond
(for forward tactics).seqCompose(first,second) runs
first
followed bysecond
(for forward tactics).- Definition Classes
- UnifyUSCalculus
-
def
seqComposeP(first: ForwardPositionTactic, second: ForwardPositionTactic): ForwardPositionTactic
seqComposeP(first,second) runs
first
followed bysecond
(for forward tactics).seqComposeP(first,second) runs
first
followed bysecond
(for forward tactics).- Definition Classes
- UnifyUSCalculus
-
val
skip: BuiltInTactic
skip is a no-op tactic that has no effect Identical to nil but different name
skip is a no-op tactic that has no effect Identical to nil but different name
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
- See also
-
def
stepAt(axiomIndex: (Expression) ⇒ Option[DerivationInfo]): DependentPositionTactic
Make the canonical simplifying proof step based at the indicated position except when an unknown decision needs to be made (e.g.
Make the canonical simplifying proof step based at the indicated position except when an unknown decision needs to be made (e.g. invariants for loops or for differential equations). Using the provided AxIndex.
- Definition Classes
- UnifyUSCalculus
- Note
Efficient source-level 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 AxIndex.
- Annotations
- @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
- Note
Efficient source-level indexing implementation.
- See also
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
lazy val
testb: BuiltInPositionTactic
testb: [?] simplifies test
[?q;]p
to an implicationq->p
-
lazy val
testd: BuiltInPositionTactic
testd: <?> simplifies test
<?q;>p
to a conjunctionq&p
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
val
todo: BuiltInTactic
A no-op tactic that as no effect but marks an open proof task.
A no-op tactic that as no effect but marks an open proof task.
- Definition Classes
- UnifyUSCalculus
- Annotations
- @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
- See also
-
def
uniformRename(ur: URename): BuiltInTactic
uniformRename(ur) renames
ur.what
tour.repl
uniformly and vice versa.uniformRename(ur) renames
ur.what
tour.repl
uniformly and vice versa.- Definition Classes
- UnifyUSCalculus
- See also
-
def
uniformRename(what: Variable, repl: Variable): BuiltInTactic
uniformRename(what,repl) renames
what
torepl
uniformly and vice versa.uniformRename(what,repl) renames
what
torepl
uniformly and vice versa.- 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): InputTactic
- Definition Classes
- UnifyUSCalculus
- See also
US()
-
def
useAt(lem: Lemma): BuiltInPositionTactic
useAt(lem)(pos) uses the given lemma at the given position in the sequent (by unifying and equivalence rewriting).
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): BuiltInPositionTactic
- Definition Classes
- UnifyUSCalculus
-
def
useAt(lem: Lemma, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): BuiltInPositionTactic
useAt(lem)(pos) uses the given lemma at the given position in the sequent (by unifying and equivalence rewriting).
useAt(lem)(pos) uses the given lemma at the given position in the sequent (by unifying and equivalence rewriting).
- key
the optional position of the key in the axiom to unify with.
- inst
optional transformation augmenting or replacing the uniform substitutions after unification with additional information.
- Definition Classes
- UnifyUSCalculus
-
def
useAt(axiom: ProvableInfo, key: PosInExpr): BuiltInPositionTactic
useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), overwriting key.
useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), overwriting key.
- key
the optional position of the key in the axiom to unify with.
- Definition Classes
- UnifyUSCalculus
-
def
useAt(axiom: AxiomInfo, inst: (Option[Subst]) ⇒ Subst): BuiltInPositionTactic
useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), with a given instantiation augmentation.
useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), with a given instantiation augmentation.
- inst
transformation augmenting or replacing the uniform substitutions after unification with additional information.
- Definition Classes
- UnifyUSCalculus
-
def
useAt(axiom: ProvableInfo, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): BuiltInPositionTactic
useAt(axiom)(pos) uses the given axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence/implicational rewriting).
useAt(axiom)(pos) uses the given axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence/implicational rewriting). Unifies the left or right part of fact with what's found at sequent(pos) and use corresponding instance to make progress by reducing to the other side.
G |- C{s(r)}, D ------------------ useAt(__l__<->r) if s=unify(c,l) G |- C{c}, D
and accordingly for implication facts that are
l->r
facts or conditional equivalencesp->(l<->r)
orp->(l->r)
facts and so on, wherel
indicates the key part of the fact. useAt automatically tries proving the required assumptions/conditions of the fact it is using.Backward Tableaux-style proof analogue of useFor().
Tactic specification:
useAt(fact)(p)(F) = let (C,c)=F(p) in case c of { s=unify(fact.left,_) => CutRight(C(s(fact.right))(p) ; <( "use cut": skip "show cut": EquivifyRight(p.top) ; CoHide(p.top) ; CE(C(_)) ; fact ) s=unify(fact.right,_) => accordingly with an extra commuteEquivRightT }
- axiom
describing what fact to use to simplify at the indicated position of the sequent
- key
the part of the Formula fact to unify the indicated position of the sequent with
- inst
Transformation for instantiating additional unmatched symbols that do not occur in fact(key). Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the most-general unifier are preferred.
- Definition Classes
- UnifyUSCalculus
useAt(AxiomInfo("[;] choice", PosInExpr(0::Nil))(0, PosInExpr(1::1::Nil)) applied to the indicated 1::1::Nil position of [x:=1;][{x'=22}] [x:=2*x;++x:=0;]x>=0 turns it into [x:=1;][{x'=22}] ([x:=2*x;]x>=0 & [x:=0;]x>=0)
- To do
could directly use prop rules instead of CE if key close to HereP if more efficient.
- See also
useFor()
Example: -
def
useAt(axiom: ProvableInfo): BuiltInPositionTactic
useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting).
useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting).
- Definition Classes
- UnifyUSCalculus
-
def
useExpansionAt(axiom: AxiomInfo): BuiltInPositionTactic
useExpansionAt(axiom)(pos) uses the given axiom at the given position in the sequent (by unifying and equivalence rewriting) in the direction that expands as opposed to simplifies operators.
useExpansionAt(axiom)(pos) uses the given axiom at the given position in the sequent (by unifying and equivalence rewriting) in the direction that expands as opposed to simplifies operators.
- Definition Classes
- UnifyUSCalculus
- See also
useAt(AxiomInfo)
-
def
useFor(fact: ProvableSig, key: PosInExpr, inst: (Subst) ⇒ Subst = us => us): ForwardPositionTactic
useFor(fact,key,inst) use the key part of the given fact forward for the selected position in the given Provable to conclude a new Provable Forward Hilbert-style proof analogue of useAtImpl().
useFor(fact,key,inst) use the key part of the given fact forward for the selected position in the given Provable to conclude a new Provable Forward Hilbert-style proof analogue of useAtImpl().
G |- C{c}, D ------------------ useFor(__l__<->r) if s=unify(c,l) G |- C{s(r)}, D
and accordingly for facts that are
l->r
facts or conditionalp->(l<->r)
orp->(l->r)
facts and so on, wherel
indicates the key part of the fact. useAt automatically tries proving the required assumptions/conditions of the fact it is using.For facts of the form
prereq -> (left<->right)
this tactic currently only uses master to prove
prereq
globally and otherwise gives up.- fact
the Provable fact whose conclusion to use to simplify at the indicated position of the sequent
- key
the part of the fact's conclusion to unify the indicated position of the sequent with
- inst
Transformation for instantiating additional unmatched symbols that do not occur in
fact.conclusion(key)
. Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the most-general unifier are preferred.
- Definition Classes
- UnifyUSCalculus
useFor(Axiom.axiom(Ax.composeb), PosInExpr(0::Nil)) applied to the indicated 1::1::Nil of
turns it into[x:=1;][{x'=22}][x:=2*x;++x:=0;]x>=0
[x:=1;][{x'=22}] ([x:=2*x;]x>=0 & [x:=0;]x>=0)
- See also
useAtImpl()
Example: -
def
useFor(axiom: ProvableInfo, inst: (Subst) ⇒ Subst): ForwardPositionTactic
- Definition Classes
- UnifyUSCalculus
-
def
useFor(pi: ProvableInfo, key: PosInExpr, inst: (Subst) ⇒ Subst): ForwardPositionTactic
useFor(pi, key) use the key part of the given axiom or provable info forward for the selected position in the given Provable to conclude a new Provable
useFor(pi, key) use the key part of the given axiom or provable info forward for the selected position in the given Provable to conclude a new Provable
- key
the optional position of the key in the axiom to unify with. Defaults to AxiomInfo.theKey
- inst
optional transformation augmenting or replacing the uniform substitutions after unification with additional information. Defaults to no change.
- Definition Classes
- UnifyUSCalculus
-
def
useFor(axiom: ProvableInfo, key: PosInExpr): ForwardPositionTactic
- Definition Classes
- UnifyUSCalculus
-
def
useFor(axiom: ProvableInfo): ForwardPositionTactic
useFor(axiom) use the given (derived) axiom/axiomatic rule forward for the selected position in the given Provable to conclude a new Provable
useFor(axiom) use the given (derived) axiom/axiomatic rule forward for the selected position in the given Provable to conclude a new Provable
- Definition Classes
- UnifyUSCalculus
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
Deprecated Value Members
-
def
by(fact: ⇒ ProvableSig, name: String = TacticFactory.ANON): BuiltInTactic
by(provable) uses the given Provable literally to continue or close the proof (if it fits to what has been proved so far)
by(provable) uses the given Provable literally to continue or close the proof (if it fits to what has been proved so far)
- fact
the Provable to drop into the proof to proceed or close it if proved.
- name
the name to use/record for the tactic
- Definition Classes
- UnifyUSCalculus
- Annotations
- @deprecated
- Deprecated
use by(ProvableInfo) instead if possible.
KeYmaera X: An aXiomatic Tactical Theorem Prover
KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics. Reasoning about complicated hybrid systems requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute tactics in parallel, and interface with partial proofs via an extensible user interface.
http://keymaeraX.org/
Concrete syntax for input language Differential Dynamic Logic
Package Structure
Main documentation entry points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.core
- KeYmaera X kernel, proof certificates, main data structuresExpression
- Differential dynamic logic expressions:Term
,Formula
,Program
Sequent
- Sequents of formulasProvable
- Proof certificates transformed by rules/axiomsRule
- Proof rules as well asUSubstOne
for (one-pass) uniform substitutions and renaming.StaticSemantics
- Static semantics with free and bound variable analysisKeYmaeraXParser
.edu.cmu.cs.ls.keymaerax.parser
- Parser and pretty printer with concrete syntax and notation for differential dynamic logic.KeYmaeraXPrettyPrinter
- Pretty printer producing concrete KeYmaera X syntaxKeYmaeraXParser
- Parser reading concrete KeYmaera X syntaxKeYmaeraXArchiveParser
- Parser reading KeYmaera X model and proof archive.kyx
filesDLParser
- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser
- Combinator parser reading KeYmaera X model and proof archive.kyx
filesedu.cmu.cs.ls.keymaerax.infrastruct
- Prover infrastructure outside the kernelUnificationMatch
- Unification algorithmRenUSubst
- Renaming Uniform Substitution quickly combining kernel's renaming and substitution.Context
- Representation for contexts of formulas in which they occur.Augmentors
- Augmenting formula and expression data structures with additional functionalityExpressionTraversal
- Generic traversal functionality for expressionsedu.cmu.cs.ls.keymaerax.bellerophon
- Bellerophon tactic language and tactic interpreterBelleExpr
- Tactic language expressionsSequentialInterpreter
- Sequential tactic interpreter for Bellerophon tacticsedu.cmu.cs.ls.keymaerax.btactics
- Bellerophon tactic library for conducting proofs.TactixLibrary
- Main KeYmaera X tactic library including many proof tactics.HilbertCalculus
- Hilbert Calculus for differential dynamic logicSequentCalculus
- Sequent Calculus for propositional and first-order logicHybridProgramCalculus
- Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
- Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
- Unification-based uniform substitution calculus underlying the other calculi[edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic]
- Forward tactic framework for conducting proofs from premises to conclusionsedu.cmu.cs.ls.keymaerax.lemma
- Lemma mechanismLemma
- Lemmas are Provables stored under a name, e.g., in files.LemmaDB
- Lemma database stored in files or database etc.edu.cmu.cs.ls.keymaerax.tools.qe
- Real arithmetic back-end solversMathematicaQETool
- Mathematica interface for real arithmetic.Z3QETool
- Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext
- Extended back-ends for noncritical ODE solving, counterexamples, algebra, simplifiers, etc.Mathematica
- Mathematica interface for ODE solving, algebra, simplification, invariant generation, etc.Z3
- Z3 interface for real arithmetic including simplifiers.Entry Points
Additional entry points and usage points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX
- Command-line launcher for KeYmaera X supports command-line argument-help
to obtain usage informationedu.cmu.cs.ls.keymaerax.btactics.AxIndex
- Axiom indexing data structures with keys and recursors for canonical proof strategies.edu.cmu.cs.ls.keymaerax.btactics.DerivationInfo
- Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.edu.cmu.cs.ls.keymaerax.bellerophon.UIIndex
- Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.edu.cmu.cs.ls.keymaerax.btactics.Ax
- Registry for derived axioms and axiomatic proof rules that are proved from the core.References
Full references on KeYmaera X are provided at http://keymaeraX.org/. The main references are the following:
1. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-265, 2017.
2. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp and André Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015.
3. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. Videos