Packages

trait SequentCalculus extends AnyRef

Sequent Calculus for propositional and first-order logic.

See also

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

Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143-189, 2008.

Linear Supertypes
AnyRef, Any
Known Subclasses
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SequentCalculus
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

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 allL(inst: Term): DependentPositionTactic

    all left: instantiate a universal quantifier in the antecedent by the concrete instance term.

  5. def allL(x: Variable, inst: Term): DependentPositionTactic

    all left: instantiate a universal quantifier for variable x in the antecedent by the concrete instance term.

  6. val allL: DependentPositionTactic

    all left: instantiate a universal quantifier in the antecedent by itself.

  7. def allLPos(instPos: Position): DependentPositionTactic

    all left: instantiate a universal quantifier in the antecedent by the term obtained from position instPos.

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

    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

  9. val andL: BuiltInLeftTactic

    &L And left: split a conjunction in the antecedent into separate assumptions (AndLeft)

  10. 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
  11. val andLi: DependentTactic
  12. val andR: BuiltInRightTactic

    &R And right: prove a conjunction in the succedent on two separate branches (AndRight)

  13. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  14. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  15. def close(a: Int, s: Int): BelleExpr
  16. def close(a: AntePos, s: SuccPos): BelleExpr

    close: closes the branch when the same formula is in the antecedent and succedent (Close)

  17. lazy val close: BelleExpr

    close: closes the branch when the same formula is in the antecedent and succedent or true or false close

  18. val closeF: BelleExpr

    closeF: closes the branch when false is in the antecedent (CloseFalse)

  19. val closeId: DependentTactic
  20. val closeIdWith: DependentPositionTactic

    closeId: closes the branch when the same formula is in the antecedent and succedent (Close)

  21. val closeT: BelleExpr

    closeT: closes the branch when true is in the succedent (CloseTrue)

  22. val cohide: DependentPositionTactic

    CoHide/coweaken whether left or right: drop all other formulas from the sequent (CoHideLeft)

  23. def cohide2: BuiltInTwoPositionTactic

    CoHide2/coweaken2 both left and right: drop all other formulas from the sequent (CoHide2)

  24. val cohideL: BuiltInLeftTactic

    CoHide/weaken left: drop all other formulas from the sequent (CoHideLeft)

  25. def cohideOnlyL: DependentPositionTactic

    Cohides in antecedent, but leaves succedent as is.

  26. def cohideOnlyR: DependentPositionTactic

    Cohides in succedent, but leaves antecedent as is.

  27. val cohideR: BuiltInRightTactic

    CoHide/weaken right: drop all other formulas from the sequent (CoHideRight)

  28. lazy val commuteEqual: DependentPositionTactic

    Commute equality a=b to b=a

  29. val commuteEquivL: BuiltInLeftTactic

    Commute equivalence on the left CommuteEquivLeft

  30. val commuteEquivR: BuiltInRightTactic

    Commute equivalence on the right CommuteEquivRight

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

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

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

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

  35. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  36. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  37. val equivL: BuiltInLeftTactic

    <->L Equiv left: use an equivalence by considering both true or both false cases (EquivLeft)

  38. val equivR: BuiltInRightTactic

    <->R Equiv right: prove an equivalence by proving both implications (EquivRight)

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

  40. val existsL: DependentPositionTactic

    exists left: Skolemize an existential quantifier in the antecedent by introducing a new name for the witness.

  41. def existsR(inst: Term): DependentPositionTactic

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

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

  43. val existsR: DependentPositionTactic

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

  44. def existsRPos(instPos: Position): DependentPositionTactic

    exists right: instantiate an existential quantifier in the succedent by a concrete term obtained from position instPos.

  45. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  46. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  47. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  48. val hide: DependentPositionTactic

    Hide/weaken whether left or right

  49. val hideL: BuiltInLeftTactic

    Hide/weaken left: weaken a formula to drop it from the antecedent (HideLeft)

  50. val hideR: BuiltInRightTactic

    Hide/weaken right: weaken a formula to drop it from the succcedent (HideRight)

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

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

  53. def implyRi(keep: Boolean = false): BuiltInTwoPositionTactic

    Inverse of implyR.

    Inverse of implyR.

      G, G' |- D, D', a -> b
    -------------------------
      G, a, G' |- D, b, D'
  54. val implyRi: AppliedBuiltinTwoPositionTactic
  55. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  56. 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

    Example:
    1.    p, q, G |- D
      ---------------- modusPonens
      p, p->q, G |- D
  57. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  58. val notL: BuiltInLeftTactic

    !L Not left: move an negation in the antecedent to the succedent (NotLeft)

  59. val notR: BuiltInRightTactic

    !R Not right: move an negation in the succedent to the antecedent (NotRight)

  60. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  61. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  62. val orL: BuiltInLeftTactic

    |L Or left: use a disjunction in the antecedent by assuming each option on separate branches (OrLeft)

  63. val orR: BuiltInRightTactic

    |R Or right: split a disjunction in the succedent into separate formulas to show alternatively (OrRight)

  64. 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''
  65. val orRi: DependentTactic
  66. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  67. def toString(): String
    Definition Classes
    AnyRef → Any
  68. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  69. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  70. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped