Packages

o

edu.cmu.cs.ls.keymaerax.btactics

TactixLibrary

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 built-in 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:

The tactic library also includes individual proof calculi:

  • HilbertCalculus: Hilbert Calculus for differential dynamic logic.
  • SequentCalculus: Sequent Calculus for propositional and first-order logic.
  • UnifyUSCalculus: Automatic unification-based Uniform Substitution Calculus with indexing.
See also

ToolProvider

edu.cmu.cs.ls.keymaerax.core.Rule

AxiomInfo

DerivedAxioms

UnifyUSCalculus

SequentCalculus

HilbertCalculus

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. 219-266, 2017.

Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TactixLibrary
  2. SequentCalculus
  3. HilbertCalculus
  4. UnifyUSCalculus
  5. AnyRef
  6. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. 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
  2. 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
  3. type Subst = RenUSubst

    The (generalized) substitutions used for unification

    The (generalized) substitutions used for unification

    Definition Classes
    UnifyUSCalculus

Value Members

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

    HilbertCalculus.derive

    Figure 3 in Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 2016.

  2. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  3. final def ##(): Int
    Definition Classes
    AnyRef → Any
  4. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  5. def CE(C: Context[Formula]): ForwardTactic

    CE(C) will wrap any equivalence left<->right or equality left=right fact it gets within context C.

    CE(C) will wrap any equivalence left<->right or equality left=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

  6. def CE(inEqPos: PosInExpr): DependentTactic

    CE(pos) at the indicated position within an equivalence reduces contextual equivalence C{left}<->C{right}to argument equivalence left<->right.

    CE(pos) at the indicated position within an equivalence reduces contextual equivalence C{left}<->C{right}to argument equivalence left<->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)

  7. def CEat(fact: ProvableSig, C: Context[Formula]): DependentPositionTactic

    CEat(fact,C) uses the equivalence left<->right or equality left=right or implication left->right fact for congruence reasoning in the given context C at the indicated position to replace right by left in that context (literally, no substitution).

    CEat(fact,C) uses the equivalence left<->right or equality left=right or implication left->right fact for congruence reasoning in the given context C at the indicated position to replace right by left in that context (literally, no substitution).

    Definition Classes
    UnifyUSCalculus
    Examples:
    1. CE(fact, Context("x>0&⎵".asFormula))(p) is equivalent to CE(fact)(p+PosInExpr(1::Nil)). Except that the former has the shape x>0&⎵ for the context starting from position p.

    2. ,
    3. CE(fact, Context("⎵".asFormula)) is equivalent to CE(fact).

    See also

    UnifyUSCalculus.CMon(PosInExpr)

    UnifyUSCalculus.CQ(PosInExpr)

    UnifyUSCalculus.CE(PosInExpr)

    CE(Context)

    useAt()

    UnifyUSCalculus.CEat(Provable)

  8. def CEat(fact: ProvableSig): DependentPositionTactic

    CEat(fact) uses the equivalence left<->right or equality left=right or implication left->right fact for congruence reasoning at the indicated position to replace right by left at indicated position (literally, no substitution).

    CEat(fact) uses the equivalence left<->right or equality left=right or implication left->right fact for congruence reasoning at the indicated position to replace right by left at indicated position (literally, no substitution). Efficient unification-free version of PosInExpr):PositionTactic

                           fact
    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
    Example:
    1. CEat(fact) is equivalent to CEat(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)

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

  10. def CMon: DependentPositionTactic

    Convenience CMon with hiding.

    Convenience CMon with hiding.

    Definition Classes
    UnifyUSCalculus
  11. def CMon(inEqPos: PosInExpr): DependentTactic

    CMon(pos) at the indicated position within an implication reduces contextual implication C{o}->C{k} to argument implication o->k for positive C.

    CMon(pos) at the indicated position within an implication reduces contextual implication C{o}->C{k} to argument implication o->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)

  12. def CQ(inEqPos: PosInExpr): DependentTactic

    CQ(pos) at the indicated position within an equivalence reduces contextual equivalence p(left)<->p(right) to argument equality left=right.

    CQ(pos) at the indicated position within an equivalence reduces contextual equivalence p(left)<->p(right) to argument equality left=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)

  13. 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
  14. 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
  15. 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 assignment x':=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 assignment x':=f(x).

    G |- [{x'=f(||)&H(||)}][x':=f(||);]p(||), D
    -------------------------------------------
    G |- [{x'=f(||)&H(||)}]p(||), D
    Definition Classes
    HilbertCalculus
    Examples:
    1. |- [{x'=1, y'=x & x>0}][y':=x;][x':=1;]x>0
      -------------------------------------------DE(1)
      |- [{x'=1, y'=x & x>0}]x>0
    2. ,
    3. |- [{x'=1}][x':=1;]x>0
      -----------------------DE(1)
      |- [{x'=1}]x>0
  16. 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

    dG

  17. 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 to q(x) -> p(x) & [x'=f(x)]p(x)'.

    Definition Classes
    HilbertCalculus
    See also

    DifferentialTactics.diffInd()

  18. 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
  19. 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
  20. 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
  21. lazy val Dassignb: DependentPositionTactic

    Dassignb: [':=] Substitute a differential assignment [x':=f]p(x') to p(f)

    Dassignb: [':=] Substitute a differential assignment [x':=f]p(x') to p(f)

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

    boxTrue

    monb with p(x)=True

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

    mond

    monb

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

    dG

    openDiffInd

    dW

    diffInvariant

    dI

    solve

  25. def QE: BelleExpr
  26. 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).

    QE: Quantifier Elimination to decide real arithmetic (after simplifying logical transformations). Applies simplifying transformations to the real arithmetic questions before solving it via RCF.

    order

    the order of variables to use during quantifier elimination

    See also

    RCF

    QE

  27. def RCF: BelleExpr

    Real-closed field arithmetic on a single formula without any extra smarts and simplifications.

    Real-closed field arithmetic on a single formula without any extra smarts and simplifications.

    See also

    QE

  28. 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 with fact.conclusion. Use that unifier as a uniform substitution to instantiate fact 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()

  29. def US(subst: USubst): BuiltInTactic
    Definition Classes
    UnifyUSCalculus
  30. 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
  31. def US(subst: USubst, fact: ProvableSig): BuiltInTactic

    US(subst, fact) reduces the proof to a proof of fact, whose uniform substitution instance under subst the current goal is.

    US(subst, fact) reduces the proof to a proof of fact, whose uniform substitution instance under subst the current goal is.

    Definition Classes
    UnifyUSCalculus
    See also

    edu.cmu.cs.ls.keymaerax.core.Provable.apply(USubst)

  32. lazy val V: DependentPositionTactic

    V: vacuous box [a]p() will be discarded and replaced by p() provided program a does not change values of postcondition p().

    V: vacuous box [a]p() will be discarded and replaced by p() provided program a does not change values of postcondition p().

    Definition Classes
    HilbertCalculus
    Note

    Unsound for hybrid games

  33. lazy val VK: DependentPositionTactic

    VK: vacuous box [a]p() will be discarded and replaced by p() provided program a does not change values of postcondition p() and provided [a]true proves, e.g., since a is a hybrid system.

    VK: vacuous box [a]p() will be discarded and replaced by p() provided program a does not change values of postcondition p() and provided [a]true proves, e.g., since a is a hybrid system.

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

    Example:
    1. maxcd = max(c,d) |- a+b <= maxcd+e
      ----------------------------------------abbrv(Variable("maxcd"))(1, 1::0::Nil)
                       |- a+b <= max(c, d) + e
  35. lazy val abs: DependentPositionTactic

    Expands absolute value using abs(x)=y <-> (x>=0&y=x | x<=0&y=-x), see EqualityTactics.abs

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

    Examples:
    1.   |- x>0
      ---------------abstractionb(1)
        |- [y:=2;]x>0
    2. ,
    3.   |- 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
    4. ,
    5.   |- \forall x x>0
      ------------------abstractionb(1)
        |- [x:=2;]x>0
  37. lazy val allDist: DependentPositionTactic
    Definition Classes
    HilbertCalculus
  38. lazy val allG: BelleExpr

    allG: all generalization rule reduces a proof of |- \forall x p(x) to proving |- p(x) in isolation

    allG: all generalization rule reduces a proof of |- \forall x p(x) to proving |- p(x) in isolation

    Definition Classes
    HilbertCalculus
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
    Examples:
    1. 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
    2. ,
    3. y>5   |- x^2>=0
      --------------------------allSkolemize(1)
      y>5   |- \forall x x^2>=0
    See also

    edu.cmu.cs.ls.keymaerax.core.Skolemize

  44. 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
  45. lazy val alphaRule: BelleExpr

    Alpha rules are propositional rules that do not split

  46. 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
  47. 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
  48. val andLi: DependentTactic
    Definition Classes
    SequentCalculus
  49. 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
  50. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  51. 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.

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

  53. def assertT(antecedents: Int, succedents: Int, msg: ⇒ String = ""): BelleExpr

    Assert that the sequent has the specified number of antecedent and succedent formulas, respectively.

  54. def assertT(cond: (Sequent) ⇒ Boolean, msg: ⇒ String): BelleExpr

    Assert that the given condition holds for the goal's sequent.

  55. lazy val assignb: DependentPositionTactic

    assignb: [:=] simplify assignment [x:=f;]p(x) by substitution p(f) or equation.

    assignb: [:=] simplify assignment [x:=f;]p(x) by substitution p(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.

    Definition Classes
    HilbertCalculus
    Examples:
    1. |- [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
    2. ,
    3. \\forall x_0 (x_0=1 -> [{x_0:=x_0+1;}*]x_0>0) |-
      -------------------------------------------------assignb(-1)
                             [x:=1;][{x:=x+1;}*]x>0 |-
    4. ,
    5. x_0=1 |- [{x_0:=x_0+1;}*]x_0>0
      ----------------------------------assignb(1)
            |- [x:=1;][{x:=x+1;}*]x>0
    6. ,
    7.        1>0 |-
      --------------------assignb(-1)
      [x:=1;]x>0 |-
    8. ,
    9. |- 1>0
      --------------------assignb(1)
      |- [x:=1;]x>0
    See also

    DLBySubst.assignEquality

  56. lazy val assignd: DependentPositionTactic

    assignd: <:=> simplify assignment <x:=f;>p(x) by substitution p(f) or equation

    assignd: <:=> simplify assignment <x:=f;>p(x) by substitution p(f) or equation

    Definition Classes
    HilbertCalculus
  57. def atomicQE: BelleExpr
  58. 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

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

    master

  60. lazy val betaRule: BelleExpr

    Beta rules are propositional rules that split

  61. def boundRename(what: Variable, repl: Variable): DependentPositionTactic

    boundRename(what,repl) renames what to repl at the indicated position (or vice versa).

    boundRename(what,repl) renames what to repl at the indicated position (or vice versa).

    Definition Classes
    UnifyUSCalculus
    See also

    edu.cmu.cs.ls.keymaerax.core.BoundRenaming

  62. lazy val box: DependentPositionTactic

    box: [.] to reduce double-negated diamond !⟨a⟩!p(x) to a box [a]p(x).

    box: [.] to reduce double-negated diamond !⟨a⟩!p(x) to a box [a]p(x).

    Definition Classes
    HilbertCalculus
  63. 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
  64. 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
  65. val boxTrue: DependentPositionTactic

    boxTrue: proves [a]true directly for hybrid systems a that are not hybrid games.

    boxTrue: proves [a]true directly for hybrid systems a that are not hybrid games.

    Definition Classes
    HilbertCalculus
  66. 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
  67. 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 called name.

    Definition Classes
    UnifyUSCalculus
    See also

    byUS()

  68. def by(lemma: Lemma, name: String): BelleExpr
    Definition Classes
    UnifyUSCalculus
  69. 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
  70. 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
  71. 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 most-general unifier are preferred.

    Definition Classes
    UnifyUSCalculus
    See also

    by()

    byUS()

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

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

  75. 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 most-general unifier are preferred.

    index

    Provides recursors to continue chase after applying an axiom from keys. Defaults to AxiomIndex.axiomIndex.

    Definition Classes
    UnifyUSCalculus
    Examples:
    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))

    2. ,
    3. 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))

    4. ,
    5. 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 search-free and, thus, quite efficient. It directly follows the axiom index information to compute follow-up positions for the chase.

    See also

    chaseFor()

    HilbertCalculus.derive

  76. def chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  77. def chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String]): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  78. 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
  79. 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
  80. 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
  81. def chaseCustomFor(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  82. 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 most-general unifier are preferred.

    Definition Classes
    UnifyUSCalculus
    Examples:
    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))

    2. ,
    3. 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))

    4. ,
    5. 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 search-free and, thus, quite efficient. It directly follows the axiom index information to compute follow-up positions for the chase.

    See also

    UnifyUSCalculus.useFor()

    HilbertCalculus.derive

    chase()

  83. 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
  84. def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  85. def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  86. 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
  87. def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  88. def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], inst: (String) ⇒ (Subst) ⇒ Subst): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  89. 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
  90. 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
  91. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  92. def close(a: Int, s: Int): BelleExpr
    Definition Classes
    SequentCalculus
  93. 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
  94. 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
  95. 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
  96. val closeId: DependentTactic
    Definition Classes
    SequentCalculus
  97. 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
  98. 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
  99. 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
  100. 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
  101. 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
  102. def cohideOnlyL: DependentPositionTactic

    Cohides in antecedent, but leaves succedent as is.

    Cohides in antecedent, but leaves succedent as is.

    Definition Classes
    SequentCalculus
  103. def cohideOnlyR: DependentPositionTactic

    Cohides in succedent, but leaves antecedent as is.

    Cohides in succedent, but leaves antecedent as is.

    Definition Classes
    SequentCalculus
  104. 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
  105. lazy val commuteEqual: DependentPositionTactic

    Commute equality a=b to b=a

    Commute equality a=b to b=a

    Definition Classes
    SequentCalculus
  106. 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
  107. val commuteEquivL: BuiltInLeftTactic

    Commute equivalence on the left CommuteEquivLeft

    Commute equivalence on the left CommuteEquivLeft

    Definition Classes
    SequentCalculus
  108. val commuteEquivR: BuiltInRightTactic

    Commute equivalence on the right CommuteEquivRight

    Commute equivalence on the right CommuteEquivRight

    Definition Classes
    SequentCalculus
  109. 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
  110. 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
  111. 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(v-1)
    --------------------------------------------------------------------------------------------
    G |- <{a}*>p, D
    variant

    The variant property or convergence property in terms of new variable v.

    Example:
    1. The variant J(v) ~> (v = z) is specified as v=="v".asVariable, variant == "v = z".asFormula

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

  114. 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
  115. 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
  116. 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
  117. 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.

    Examples:
    1. 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
    2. ,
    3. 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
    4. ,
    5. 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()

  118. 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*y-b

    r

    the optional equivalent new postcondition to prove that can mention y; keeps p(x) if omitted.

    Example:
    1. 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)

  119. 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
    Examples:
    1. proveBy("x^2>=2->[{x'=x^3}]x^2>=2".asFormula, implyR(1) &
        diffInd()(1) & QE
      )
    2. ,
    3. 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
    4. ,
    5. x>=5, true |- x>=5    x>=5, true |- [{x'=2}](x>=5)'
      ---------------------------------------------------diffInd(qeTool, 'none)(1)
      x>=5 |- [{x'=2}]x>=5
    6. ,
    7. x>=5, true |- x>=5    true |- [{x':=2}]x'>=0
      --------------------------------------------diffInd(qeTool, 'diffInd)(1)
      x>=5 |- [{x'=2}]x>=5
    8. ,
    9.      *
      ---------------------diffInd(qeTool, 'full)(1)
      x>=5 |- [{x'=2}]x>=5
  120. def dR(formula: Formula, hide: Boolean = true): DependentPositionTactic

    Refine top-level 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 top-level 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

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

  122. def debug(s: ⇒ Any): BuiltInTactic

    debug(s) sprinkles debug message s into the output and the ProofNode information

  123. def debugAt(s: ⇒ Any): BuiltInPositionTactic

    debugAt(s) sprinkles debug message s into the output and the ProofNode information

  124. 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
    Example:
    1. 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

    UnifyUSCalculus.chase

  125. lazy val diamond: DependentPositionTactic

    diamond: <.> reduce double-negated box ![a]!p(x) to a diamond ⟨a⟩p(x).

    diamond: <.> reduce double-negated box ![a]!p(x) to a diamond ⟨a⟩p(x).

    Definition Classes
    HilbertCalculus
  126. lazy val diamondOr: DependentPositionTactic

    diamondOr: splits ⟨a⟩(p|q) into ⟨a⟩p | ⟨a⟩q

    diamondOr: splits ⟨a⟩(p|q) into ⟨a⟩p | ⟨a⟩q

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

    Examples:
    1. 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
    2. ,
    3. x>0, x_0=x |- [{x'=2&x>x_0}]x>=0
      ---------------------------------diffInvariant("x>old(x)".asFormula)(1)
             x>0 |- [{x'=2}]x>=0
    4. ,
    5. x>0 |- [{x'=2&x>0}]x>=0
      ------------------------diffInvariant("x>0".asFormula)(1)
      x>0 |- [{x'=2}]x>=0
    See also

    dI

    dC

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

    Example:
    1.      *
      ------------------------- DV(1)
      a()>0 |- <{x'=a()}>x>=b()
  129. def discreteGhost(t: Term, ghost: Option[Variable] = None): DependentPositionTactic

    iG discreteGhost: introduces a discrete ghost called ghost defined as term t; if ghost is None the tactic chooses a name by inspecting t.

    iG discreteGhost: introduces a discrete ghost called ghost defined as term t; if ghost is None the tactic chooses a name by inspecting t.

    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.

    Examples:
    1. |- [z:=2;][y:=5;]x>0
      ---------------------discreteGhost("0".asTerm, Some("y".asVariable))(1, 1::Nil)
      |- [z:=2;]x>0
    2. ,
    3. |- [y_0:=y;]x>0
      ----------------discreteGhost("y".asTerm)(1)
      |- x>0
  130. 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

    skip

  131. 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
  132. 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
  133. 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.

  134. def either(left: ForwardTactic, right: ForwardTactic): ForwardTactic

    either(left,right) runs left if successful and right otherwise (for forward tactics).

    either(left,right) runs left if successful and right otherwise (for forward tactics).

    Definition Classes
    UnifyUSCalculus
  135. def eitherP(left: ForwardPositionTactic, right: ForwardPositionTactic): ForwardPositionTactic

    eitherP(left,right) runs left if successful and right otherwise (for forward tactics).

    eitherP(left,right) runs left if successful and right otherwise (for forward tactics).

    Definition Classes
    UnifyUSCalculus
  136. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  137. def eqL2R(eqPos: AntePosition): DependentPositionTactic
  138. def eqL2R(eqPos: Int): DependentPositionTactic

    Rewrites free occurrences of the left-hand side of an equality into the right-hand side at a specific position.

    Rewrites free occurrences of the left-hand side of an equality into the right-hand 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.

    Example:
    1. x=0 |- 0*y=0, x+1>0
      ---------------------eqL2R(-1)(1)
      x=0 |- x*y=0, x+1>0
  139. def eqR2L(eqPos: AntePosition): DependentPositionTactic
  140. def eqR2L(eqPos: Int): DependentPositionTactic

    Rewrites free occurrences of the right-hand side of an equality into the left-hand side at a specific position (EqualityTactics.eqR2L).

  141. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  142. 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
  143. 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
  144. 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
  145. def errorT(msg: ⇒ String): BuiltInTactic

    errorT raises an error upon executing this tactic, stopping processing

  146. def exhaustiveEqL2R(hide: Boolean = false): DependentPositionTactic
  147. lazy val exhaustiveEqL2R: DependentPositionTactic

    Rewrites free occurrences of the left-hand side of an equality into the right-hand side exhaustively (EqualityTactics.exhaustiveEqL2R).

  148. def exhaustiveEqR2L(hide: Boolean = false): DependentPositionTactic
  149. lazy val exhaustiveEqR2L: DependentPositionTactic

    Rewrites free occurrences of the right-hand side of an equality into the left-hand side exhaustively (EqualityTactics.exhaustiveEqR2L).

  150. lazy val existsE: DependentPositionTactic
    Definition Classes
    HilbertCalculus
  151. 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
  152. def existsR(inst: Term): DependentPositionTactic

    exists right: instantiate an existential quantifier in the succedent by a concrete instance inst as a witness

    exists right: instantiate an existential quantifier in the succedent by a concrete instance inst as a witness

    Definition Classes
    SequentCalculus
  153. 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 witness

    exists right: instantiate an existential quantifier for x in the succedent by a concrete instance inst as a witness

    Definition Classes
    SequentCalculus
  154. 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
  155. 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
  156. 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
  157. val fail: BelleExpr

    fail is a tactic that always fails

    fail is a tactic that always fails

    See also

    skip

  158. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  159. def findCounterExample(formula: Formula): Option[Map[NamedSymbol, Expression]]

    Finds a counter example, indicating that the specified formula is not valid.

  160. def fromAxIndex(s: String): (ProvableSig, PosInExpr, List[PosInExpr])
    Definition Classes
    UnifyUSCalculus
  161. 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
    Examples:
    1. 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
    2. ,
    3. genUseLbl:        genShowLbl:
      |- [x:=2;]x>1     x>1 |- [y:=x;]y>1
      ------------------------------------generalize("x>1".asFormula)(1)
      |- [x:=2;][y:=x;]y>1
  162. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  163. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  164. def heuQE: BelleExpr
  165. def heuQEPO(po: Ordering[Variable]): BelleExpr
  166. val hide: DependentPositionTactic

    Hide/weaken whether left or right

    Hide/weaken whether left or right

    Definition Classes
    SequentCalculus
  167. 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
  168. 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
  169. 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
  170. def ifThenElse(cond: (Sequent, Position) ⇒ Boolean, thenT: BelleExpr, elseT: BelleExpr): DependentPositionTactic

    ifThenElse(cond,thenT,elseT) runs thenT if cond holds at position and elseT otherwise.

  171. def ifThenElse(cond: (ProvableSig) ⇒ Boolean, thenT: ForwardTactic, elseT: ForwardTactic): ForwardTactic

    ifThenElse(cond,thenT,elseT) runs thenT if cond holds and elseT otherwise (for forward tactics).

    ifThenElse(cond,thenT,elseT) runs thenT if cond holds and elseT otherwise (for forward tactics).

    Definition Classes
    UnifyUSCalculus
  172. def ifThenElseP(cond: (Position) ⇒ (ProvableSig) ⇒ Boolean, thenT: ForwardPositionTactic, elseT: ForwardPositionTactic): ForwardPositionTactic

    ifThenElseP(cond,thenT,elseT) runs thenT if cond holds and elseT otherwise (for forward tactics).

    ifThenElseP(cond,thenT,elseT) runs thenT if cond holds and elseT otherwise (for forward tactics).

    Definition Classes
    UnifyUSCalculus
  173. val implyL: BuiltInLeftTactic

    ->L Imply left: use an implication in the antecedent by proving its left-hand side on one branch and using its right-hand side on the other branch (ImplyLeft)

    ->L Imply left: use an implication in the antecedent by proving its left-hand side on one branch and using its right-hand side on the other branch (ImplyLeft)

    Definition Classes
    SequentCalculus
  174. val implyR: BuiltInRightTactic

    ->R Imply right: prove an implication in the succedent by assuming its left-hand side and proving its right-hand side (ImplyRight)

    ->R Imply right: prove an implication in the succedent by assuming its left-hand side and proving its right-hand side (ImplyRight)

    Definition Classes
    SequentCalculus
  175. 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
  176. val implyRi: AppliedBuiltinTwoPositionTactic
    Definition Classes
    SequentCalculus
  177. 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

    InvariantGenerator

  178. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  179. lazy val iterateb: DependentPositionTactic

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

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

    Definition Classes
    HilbertCalculus
  180. lazy val iterated: DependentPositionTactic

    iterated: <*> prove a property of a loop ⟨{a}*⟩p(x) by unrolling it once p(x) | ⟨a⟩⟨{a}*⟩p(x)

    iterated: <*> prove a property of a loop ⟨{a}*⟩p(x) by unrolling it once p(x) | ⟨a⟩⟨{a}*⟩p(x)

    Definition Classes
    HilbertCalculus
  181. def label(s: String): BelleExpr

    Call/label the current proof branch by the top-level label s.

    Call/label the current proof branch by the top-level label s.

    See also

    sublabel()

    Idioms.<()

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

    BelleLabels

    sublabel()

    Idioms.<()

  183. def lazyUseAt(lemmaName: String, key: PosInExpr): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  184. 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
  185. def let(abbr: Expression, value: Expression, inner: BelleExpr): BelleExpr

    Let(abbr, value, inner) alias let abbr=value in inner abbreviates value by abbr in the provable and proceeds with an internal proof by tactic inner, resuming to the outer proof by a uniform substitution of value for abbr of the resulting provable.

    Let(abbr, value, inner) alias let abbr=value in inner abbreviates value by abbr in the provable and proceeds with an internal proof by tactic inner, resuming to the outer proof by a uniform substitution of value for abbr of the resulting provable.

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

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

    Examples:
    1. 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
    2. ,
    3. 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.

  188. def loopPostMaster(gen: Generator.Generator[Formula]): DependentPositionTactic

    loopPostMaster: search-and-rescue style automatic loop induction based on successive generator gen.

    loopPostMaster: search-and-rescue 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. 219-266, 2017. Example 32.

  189. 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. 219-266, 2017. Example 32.

    loopauto

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

  191. 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 result false of a QE step at the leaves is kept or undone (i.e., reverted to the QE input sequent).

    See also

    auto

  192. def master(loop: AtPosition[_ <: BelleExpr], odeR: AtPosition[_ <: BelleExpr], keepQEFalse: Boolean): BelleExpr

    Master/auto implementation with tactic loop for nondeterministic repetition and odeR for differential equations in the succedent.

    Master/auto implementation with tactic loop for nondeterministic repetition and odeR for differential equations in the succedent. keepQEFalse indicates whether or not QE results "false" at the proof leaves should be kept or undone.

  193. lazy val max: DependentPositionTactic

    Expands maximum function using max(x,y)=z <-> (x>=y&z=x | x<=y&z=y), see EqualityTactics.minmax

  194. lazy val min: DependentPositionTactic

    Expands minimum function using min(x,y)=z <-> (x<=y&z=x | x>=y&z=y), see EqualityTactics.minmax

  195. 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
    Example:
    1.    p, q, G |- D
      ---------------- modusPonens
      p, p->q, G |- D
  196. lazy val monb: BelleExpr

    monb: Monotone [a]p(x) |- [a]q(x) reduces to proving p(x) |- q(x)

    monb: Monotone [a]p(x) |- [a]q(x) reduces to proving p(x) |- q(x)

    Definition Classes
    HilbertCalculus
  197. lazy val mond: BelleExpr

    mond: Monotone ⟨a⟩p(x) |- ⟨a⟩q(x) reduces to proving p(x) |- q(x)

    mond: Monotone ⟨a⟩p(x) |- ⟨a⟩q(x) reduces to proving p(x) |- q(x)

    Definition Classes
    HilbertCalculus
  198. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  199. val nil: BelleExpr

    nil=skip is a no-op tactic that has no effect

  200. def normalize(beta: AtPosition[_ <: BelleExpr]*): BelleExpr

    Normalize to sequent form.

    Normalize to sequent form. Keeps branching factor of tacticChase restricted to beta rules.

  201. lazy val normalize: BelleExpr

    Normalize to sequent form.

    Normalize to sequent form. Keeps branching factor of tacticChase restricted to orL, implyL, equivL, andR, and equivR.

  202. 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
  203. 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
  204. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  205. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  206. 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)

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

  208. def onAll(e: BelleExpr): BelleExpr

    OnAll(e) == <(e, ..., e) runs tactic e on all current branches.

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

    Examples:
    1. proveBy("x^2>9->[{x'=x^4}]x^2>9".asFormula, implyR(1) &
        openDiffInd()(1)
      )
    2. ,
    3.      *
      ---------------------openDiffInd(1)
      x^3>5 |- [{x'=x^3+x^4}]x^3>5
    4. ,
    5.      *
      ---------------------openDiffInd(1)
      x^2>5 |- [{x'=x^3+x^4}]x^2>5
  210. 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
  211. 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
  212. 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
  213. val orRi: DependentTactic
    Definition Classes
    SequentCalculus
  214. 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

  215. def positionOf(fml: Formula): PosInExpr

    The position of here() in the formula fml.

    The position of here() in the formula fml.

    returns

    The term or formula position where here() occurs in fml.

    Example:
    1. 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 if here() does not occur in fml.

  216. 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
    Examples:
    1. 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
    2. ,
    3. 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
  217. val prop: BelleExpr
  218. 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

    Example:
    1. import StringConverter._
      import TactixLibrary._
      val proof = TactixLibrary.proveBy("(p()|q()->r()) <-> (p()->r())&(q()->r())".asFormula, prop)
    See also

    TactixLibrary.by(Provable)

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

    Example:
    1. 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

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

  221. 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
  222. 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
  223. def seqCompose(first: ForwardTactic, second: ForwardTactic): ForwardTactic

    seqCompose(first,second) runs first followed by second (for forward tactics).

    seqCompose(first,second) runs first followed by second (for forward tactics).

    Definition Classes
    UnifyUSCalculus
  224. def seqComposeP(first: ForwardPositionTactic, second: ForwardPositionTactic): ForwardPositionTactic

    seqComposeP(first,second) runs first followed by second (for forward tactics).

    seqComposeP(first,second) runs first followed by second (for forward tactics).

    Definition Classes
    UnifyUSCalculus
  225. val skip: BelleExpr

    nil=skip is a no-op tactic that has no effect

    nil=skip is a no-op tactic that has no effect

    See also

    done

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

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

  228. val step: DependentPositionTactic

    step: one canonical simplifying proof step at the indicated formula/term position (unless @invariant etc needed)

  229. 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 source-level indexing implementation.

    See also

    AxiomIndex

  230. 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 source-level indexing implementation.

    See also

    AxiomIndex

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

  232. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  233. def tacticChase(tacticIndex: TacticIndex = new DefaultTacticIndex)(restrictTo: AtPosition[_ <: BelleExpr]*): BelleExpr

    Exhaustively (depth-first) apply tactics from the tactic index, restricted to the tactics in restrictTo, to chase away.

    Exhaustively (depth-first) apply tactics from the tactic index, restricted to the tactics in restrictTo, to chase away. Unlike chase, tacticChase will use propositional proof rules and possibly branch

    See also

    chase

  234. lazy val testb: DependentPositionTactic

    testb: [?] simplifies test [?q;]p to an implication q->p

    testb: [?] simplifies test [?q;]p to an implication q->p

    Definition Classes
    HilbertCalculus
  235. lazy val testd: DependentPositionTactic

    testd: <?> simplifies test <?q;>p to a conjunction q&p

    testd: <?> simplifies test <?q;>p to a conjunction q&p

    Definition Classes
    HilbertCalculus
  236. 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
  237. def toString(): String
    Definition Classes
    AnyRef → Any
  238. 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.

    Examples:
    1.                 *
                      ---------------
      a<c |- a<c      |- c+0=c
      -------------------------------transform("c".asFormula)(1, 1::Nil)
      a<c |- a<c+0
    2. ,
    3.                               *
                               ---------------------
      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
    4. ,
    5.                 *
                      --------------
      a<b |- a<b      |- a<b -> b>a
      ------------------------------ transform("a.asFormula)(1)
      a<b |- b>a
  239. 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.

  240. def uniformRename(ur: URename): InputTactic

    uniformRename(ur) renames ur.what to ur.repl uniformly and vice versa.

    uniformRename(ur) renames ur.what to ur.repl uniformly and vice versa.

    Definition Classes
    UnifyUSCalculus
    See also

    edu.cmu.cs.ls.keymaerax.core.UniformRenaming

  241. def uniformRename(what: Variable, repl: Variable): InputTactic

    uniformRename(what,repl) renames what to repl uniformly and vice versa.

    uniformRename(what,repl) renames what to repl uniformly and vice versa.

    Definition Classes
    UnifyUSCalculus
    See also

    edu.cmu.cs.ls.keymaerax.core.UniformRenaming

  242. def uniformRenameF(what: Variable, repl: Variable): ForwardTactic

    uniformRenameF(what,repl) renames what to repl uniformly (for forward tactics).

    uniformRenameF(what,repl) renames what to repl uniformly (for forward tactics).

    Definition Classes
    UnifyUSCalculus
  243. def uniformSubstitute(subst: USubst): BuiltInTactic

    Definition Classes
    UnifyUSCalculus
    See also

    US()

  244. def useAt(axiom: ProvableInfo, key: PosInExpr): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  245. def useAt(axiom: ProvableInfo, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  246. 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
  247. def useAt(axiom: String, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  248. def useAt(axiom: String, key: PosInExpr): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  249. 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
  250. 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
  251. def useAt(lem: Lemma, key: PosInExpr): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  252. 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
  253. def useExpansionAt(axiom: String, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  254. 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
  255. 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
  256. 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 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 Hilbert-style 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 conditional p->(l<->r) or p->(l->r) facts and so on, where l 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
    Example:
    1. useFor(Axiom.axiom("[;] compose"), PosInExpr(0::Nil)) applied to the indicated 1::1::Nil 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)

    See also

    edu.cmu.cs.ls.keymaerax.btactics

    useAt()

  257. 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
  258. 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
  259. 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
  260. 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 tactic adapt.

    useLemma(lemma, tactic) applies the lemma, optionally adapting the lemma formula to the current subgoal using the tactic adapt. Literal lemma application if adapt is None.

  261. 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 tactic adapt.

    useLemma(lemmaName, tactic) applies the lemma identified by lemmaName, optionally adapting the lemma formula to the current subgoal using the tactic adapt. Literal lemma application if adapt is None.

  262. def useLemmaAt(lemmaName: String, key: Option[PosInExpr]): DependentPositionWithAppliedInputTactic

    Applies the lemma by matching key in the lemma with the tactic position.

  263. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  264. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  265. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  266. 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

    abstractionb

Inherited from SequentCalculus

Inherited from HilbertCalculus

Inherited from UnifyUSCalculus

Inherited from AnyRef

Inherited from Any

Ungrouped