Packages

trait HilbertCalculus extends UnifyUSCalculus

Hilbert Calculus for differential dynamic logic.

Provides the axioms and axiomatic proof rules from Figure 2 and Figure 3 in: Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 2016.

See also

edu.cmu.cs.ls.keymaerax.btactics.DerivedAxioms

edu.cmu.cs.ls.keymaerax.core.AxiomBase

HilbertCalculus.derive()

HilbertCalculus.stepAt()

Andre Platzer. The complete proof theory of hybrid systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 541-550. IEEE 2012

Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. IEEE 2012

Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980

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.

Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.

Linear Supertypes
UnifyUSCalculus, AnyRef, Any
Known Subclasses
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. HilbertCalculus
  2. UnifyUSCalculus
  3. AnyRef
  4. 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. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. 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

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

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

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

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

  9. def CMon: DependentPositionTactic

    Convenience CMon with hiding.

    Convenience CMon with hiding.

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

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

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

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

  14. 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
    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
  15. 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)'.

    See also

    DifferentialTactics.diffInd()

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

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

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

  19. lazy val Dassignb: DependentPositionTactic

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

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

    Note

    Unsound for hybrid games

    See also

    boxTrue

    monb with p(x)=True

  21. lazy val K: DependentPositionTactic

    K: modal modus ponens (hybrid systems)

    K: modal modus ponens (hybrid systems)

    Note

    Use with care since limited to hybrid systems. Use monb instead.

    See also

    mond

    monb

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

  23. def US(subst: USubst): BuiltInTactic
    Definition Classes
    UnifyUSCalculus
  24. 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
  25. 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)

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

    Note

    Unsound for hybrid games

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

  28. lazy val allDist: DependentPositionTactic
  29. lazy val allG: BelleExpr

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

  30. lazy val allV: DependentPositionTactic

    allV: vacuous \forall x p() will be discarded and replaced by p() provided x does not occur in p().

  31. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  32. 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.

    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

  33. lazy val assignd: DependentPositionTactic

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

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

  35. lazy val box: DependentPositionTactic

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

  36. lazy val boxAnd: DependentPositionTactic

    boxAnd: splits [a](p&q) into [a]p & [a]q

  37. lazy val boxImpliesAnd: DependentPositionTactic

    boxImpliesAnd: splits [a](p->q&r) into [a](p->q) & [a](p->r)

  38. val boxTrue: DependentPositionTactic

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

  39. 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
  40. 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()

  41. def by(lemma: Lemma, name: String): BelleExpr
    Definition Classes
    UnifyUSCalculus
  42. 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
  43. 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
  44. 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()

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

  46. 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
  47. 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()

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

  49. def chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  50. def chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String]): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  51. 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
  52. 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
  53. 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
  54. def chaseCustomFor(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  55. 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()

  56. 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
  57. def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  58. def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  59. 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
  60. def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  61. def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], inst: (String) ⇒ (Subst) ⇒ Subst): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  62. lazy val choiceb: DependentPositionTactic

    choiceb: [++] handles both cases of a nondeterministic choice [a++b]p(x) separately [a]p(x) & [b]p(x)

  63. lazy val choiced: DependentPositionTactic

    choiced: <++> handles both cases of a nondeterministic choice ⟨a++b⟩p(x) separately ⟨a⟩p(x) | ⟨b⟩p(x)

  64. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  65. 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
  66. lazy val composeb: DependentPositionTactic

    composeb: [;] handle both parts of a sequential composition [a;b]p(x) one at a time [a][b]p(x)

  67. lazy val composed: DependentPositionTactic

    composed: <;> handle both parts of a sequential composition ⟨a;b⟩p(x) one at a time ⟨a⟩⟨b⟩p(x)

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

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

    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

  70. lazy val diamond: DependentPositionTactic

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

  71. lazy val diamondOr: DependentPositionTactic

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

  72. lazy val dualb: DependentPositionTactic

    dualb: [d] handle dual game [{a}d]p(x) by ![a]!p(x)

  73. lazy val duald: DependentPositionTactic

    duald: <d> handle dual game ⟨{a}d⟩p(x) by !⟨a⟩!p(x)

  74. 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
  75. 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
  76. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  77. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  78. lazy val existsE: DependentPositionTactic
  79. lazy val existsV: DependentPositionTactic

    existsV: vacuous \exists x p() will be discarded and replaced by p() provided x does not occur in p().

  80. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  81. def fromAxIndex(s: String): (ProvableSig, PosInExpr, List[PosInExpr])
    Definition Classes
    UnifyUSCalculus
  82. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  83. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  84. 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
  85. 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
  86. 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
  87. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  88. lazy val iterateb: DependentPositionTactic

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

  89. lazy val iterated: DependentPositionTactic

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

  90. def lazyUseAt(lemmaName: String, key: PosInExpr): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  91. 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
  92. 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
  93. lazy val monb: BelleExpr

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

  94. lazy val mond: BelleExpr

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

  95. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  96. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  97. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  98. lazy val randomb: DependentPositionTactic

    randomb: [:*] simplify nondeterministic assignment [x:=*;]p(x) to a universal quantifier \forall x p(x)

  99. lazy val randomd: DependentPositionTactic

    randomd: <:*> simplify nondeterministic assignment <x:=*;>p(x) to an existential quantifier \exists x p(x)

  100. 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
  101. 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
  102. 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

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

    Note

    Efficient source-level indexing implementation.

    See also

    AxiomIndex

  104. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  105. lazy val testb: DependentPositionTactic

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

  106. lazy val testd: DependentPositionTactic

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

  107. def toString(): String
    Definition Classes
    AnyRef → Any
  108. 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

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

  110. 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
  111. def uniformSubstitute(subst: USubst): BuiltInTactic

    Definition Classes
    UnifyUSCalculus
    See also

    US()

  112. def useAt(axiom: ProvableInfo, key: PosInExpr): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  113. def useAt(axiom: ProvableInfo, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  114. 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
  115. def useAt(axiom: String, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  116. def useAt(axiom: String, key: PosInExpr): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  117. 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
  118. 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
  119. def useAt(lem: Lemma, key: PosInExpr): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  120. 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
  121. def useExpansionAt(axiom: String, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
    Definition Classes
    UnifyUSCalculus
  122. 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
  123. 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
  124. 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()

  125. 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
  126. 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
  127. 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
  128. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  129. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  130. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  131. 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.

    See also

    HilbertCalculus.derive

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

Inherited from UnifyUSCalculus

Inherited from AnyRef

Inherited from Any

Ungrouped