Packages

trait SequentCalculus extends AnyRef

Sequent Calculus for propositional and first-order logic.

See also

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

Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.

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

TactixLibrary

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(e: Term): DependentPositionWithAppliedInputTactic
  5. def allL(e: Option[Term]): DependentPositionWithAppliedInputTactic

    all left: instantiate a universal quantifier in the antecedent by the concrete instance e (itself if None).

    all left: instantiate a universal quantifier in the antecedent by the concrete instance e (itself if None).

    Annotations
    @Tactic( x$481 , x$485 , x$486 , x$483 , x$484 , x$487 , x$488 , x$489 , x$490 , x$491 , x$482 , x$492 )
  6. def allL(x: Variable, inst: Term): BuiltInPositionTactic

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

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

    p(inst), G |- D
    ------------------------ ∀L
    \forall x p(x), G |- D
  7. val allL: DependentPositionTactic

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

  8. def allLPos(instPos: Position): DependentPositionTactic

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

  9. def allLkeep(e: Term): DependentPositionWithAppliedInputTactic

    all left keep: keeping around the quantifier, instantiate a universal quantifier in the antecedent by the concrete instance e.

    all left keep: keeping around the quantifier, instantiate a universal quantifier in the antecedent by the concrete instance e.

    \forll x p(x), G, p(e) |- D
    --------------------------- ∀L
    \forall x p(x), G |- D
    Annotations
    @Tactic( x$505 , x$509 , x$510 , x$507 , x$508 , x$511 , x$512 , x$513 , x$514 , x$515 , x$506 , x$516 )
  10. def allLmon(q: Formula): DependentPositionWithAppliedInputTactic

    Universal monotonicity in antecedent: replace p(x) with a characteristic property q(x).

    Universal monotonicity in antecedent: replace p(x) with a characteristic property q(x).

    Use:                      Show:
    G, \forall x q(x) |- D    G, p(x) |- D, q(x)
    -------------------------------------------- M∀L
    G, \forall x p(x) |- D
    Annotations
    @Tactic( x$493 , x$497 , x$498 , x$495 , x$496 , x$499 , x$500 , x$501 , x$502 , x$503 , x$494 , x$504 )
  11. val allR: BuiltInPositionTactic

    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.

    G |- p(x), D
    ----------------------- (Skolemize) provided x not in G,D
    G |- \forall x p(x), D
    Annotations
    @Tactic( x$217 , x$220 , x$221 , x$218 , x$219 , x$222 , x$223 , x$224 , x$225 , x$226 , x$227 , x$228 )
    Examples:
    1. y>5   |- x^2>=0
      --------------------------allSkolemize(1)
      y>5   |- \forall x x^2>=0
    2. ,
    3. Uniformly renames other occurrences of the quantified variable in the context on demand to avoid SkolemClashException.

      x_0>0 |- x^2>=0
      --------------------------allSkolemize(1)
      x>0   |- \forall x x^2>=0
    See also

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

  12. def allRi(t: Term, x: Option[Variable]): DependentPositionWithAppliedInputTactic
    Annotations
    @Tactic( x$469 , x$474 , x$475 , x$471 , x$472 , x$476 , x$477 , x$473 , x$478 , x$479 , x$470 , x$480 )
  13. def alphaRen(what: Variable, to: Variable): DependentPositionWithAppliedInputTactic

    Alpha bound renaming of what to to at a specific position (for quantifier/assignment/ode).

    Alpha bound renaming of what to to at a specific position (for quantifier/assignment/ode). Variable to must not occur free at the applied position.

    Annotations
    @Tactic( x$565 , x$570 , x$566 , x$567 , x$568 , x$571 , x$572 , x$573 , x$574 , x$575 , x$569 , x$576 )
    Example:
    1. x=y |- [{y'=y}]y>=0      x=y |- [{x'=x}]x>=0, x=y
      ------------------------------------------------- alphaRen("x","y",1)
      x=y |- [{x'=x}]x>=0
  14. def alphaRenAll(what: Variable, to: Variable): InputTactic

    Alpha renaming of what to to everywhere in the sequent.

    Alpha renaming of what to to everywhere in the sequent. Formulas that have variable to occur free are excluded from the renaming.

    Annotations
    @Tactic( x$577 , x$582 , x$578 , x$579 , x$580 , x$583 , x$584 , x$585 , x$586 , x$587 , x$581 , x$588 )
    Example:
    1. [y:=0;]y>=0 |- [{y'=y}]y>=0, [x:=y;]x=y      [x:=0;]x>=0 |- [{x'=x}]x>=0, x:=y;]x=y, x=y
      ---------------------------------------------------------------------------------------- alphaRenAll("x","y",1)
      [x:=0;]x>=0 |- [{x'=x}]x>=0, [x:=y;]x=y
  15. val alphaRenAllBy: DependentPositionTactic

    Alpha renaming everywhere in the sequent using an equality at a specific position in the antecedent.

    Alpha renaming everywhere in the sequent using an equality at a specific position in the antecedent.

    Annotations
    @Tactic( x$589 , x$593 , x$590 , x$592 , x$591 , x$594 , x$595 , x$596 , x$597 , x$598 , x$599 , x$600 )
  16. val andL: CoreLeftTactic

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

    Annotations
    @Tactic( x$241 , x$244 , x$245 , x$242 , x$243 , x$246 , x$247 , x$248 , x$249 , x$250 , x$251 , x$252 )
  17. def andLi(keepLeft: Boolean): BuiltInTwoPositionTactic

    Inverse of andL.

    Inverse of andL.

      G, G', G'', a&b  |- D
    -------------------------
      G, a, G', b, G'' |- D
  18. val andLi: AppliedBuiltinTwoPositionTactic
  19. val andR: DependentPositionTactic

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

    Annotations
    @Tactic( x$169 , x$172 , x$173 , x$170 , x$171 , x$174 , x$175 , x$176 , x$177 , x$178 , x$179 , x$180 )
  20. val andRRule: CoreRightTactic
    Annotations
    @Tactic( x$361 , x$364 , x$365 , x$362 , x$363 , x$366 , x$367 , x$368 , x$369 , x$370 , x$371 , x$372 )
  21. val applyEqualities: BuiltInTactic

    Rewrites all atom equalities in the assumptions.

  22. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  23. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  24. def close(a: Int, s: Int): BelleExpr
  25. val close: BuiltInTactic

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

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

           *
    ------------------ (Id)
      p, G |- p, D
          *
    ------------------ (close true)
      G |- true, D
           *
    ------------------ (close false)
      false, G |- D
    Annotations
    @Tactic( x$157 , x$161 , x$158 , x$159 , x$160 , x$162 , x$163 , x$164 , x$165 , x$166 , x$167 , x$168 )
  26. val closeF: BuiltInTactic

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

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

           *
    ------------------ (close false)
      false, G |- D
    Annotations
    @Tactic( x$325 , x$329 , x$326 , x$327 , x$328 , x$330 , x$331 , x$332 , x$333 , x$334 , x$335 , x$336 )
  27. val closeId: BuiltInTwoPositionTactic

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

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

           *
    ------------------ (Id)
      p, G |- p, D
    Annotations
    @Tactic( x$123 , x$121 , x$122 , x$124 , x$125 , x$126 , x$127 , x$128 , x$129 , x$130 , x$131 , x$132 )
  28. val closeIdWith: BuiltInPositionTactic

    closeIdWith: closes the branch with the formula at the given position when the same formula is in the antecedent and succedent (Close)

    closeIdWith: closes the branch with the formula at the given position when the same formula is in the antecedent and succedent (Close)

    Annotations
    @Tactic( x$305 , x$304 , x$301 , x$302 , x$303 , x$306 , x$307 , x$308 , x$309 , x$310 , x$311 , x$312 )
  29. val closeT: BuiltInTactic

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

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

          *
    ------------------ (close true)
      G |- true, D
    Annotations
    @Tactic( x$73 , x$77 , x$74 , x$75 , x$76 , x$78 , x$79 , x$80 , x$81 , x$82 , x$83 , x$84 )
  30. val cohide: BuiltInPositionTactic

    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)

    Annotations
    @Tactic( x$229 , x$233 , x$230 , x$231 , x$232 , x$234 , x$235 , x$236 , x$237 , x$238 , x$239 , x$240 )
  31. val 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)

    Annotations
    @Tactic( "WLR" , "coHide2" , "Co-Weaken Both" , "P |- Q" , "Γ, P |- Q, Δ" , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
  32. val cohideL: CoreLeftTactic

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

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

    Annotations
    @Tactic( x$349 , x$353 , x$350 , x$351 , x$352 , x$354 , x$355 , x$356 , x$357 , x$358 , x$359 , x$360 )
  33. val cohideOnlyL: BuiltInLeftTactic

    Cohides in antecedent, but leaves succedent as is.

    Cohides in antecedent, but leaves succedent as is.

    Annotations
    @Tactic( x$277 , x$281 , x$278 , x$279 , x$280 , x$282 , x$283 , x$284 , x$285 , x$286 , x$287 , x$288 )
  34. val cohideOnlyR: BuiltInRightTactic

    Cohides in succedent, but leaves antecedent as is.

    Cohides in succedent, but leaves antecedent as is.

    Annotations
    @Tactic( x$313 , x$317 , x$314 , x$315 , x$316 , x$318 , x$319 , x$320 , x$321 , x$322 , x$323 , x$324 )
  35. val cohideR: CoreRightTactic

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

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

    Annotations
    @Tactic( x$85 , x$89 , x$86 , x$87 , x$88 , x$90 , x$91 , x$92 , x$93 , x$94 , x$95 , x$96 )
  36. lazy val commuteEqual: BuiltInPositionTactic

    Commute equality a=b to b=a

    Commute equality a=b to b=a

    Annotations
    @Tactic( x$193 , x$196 , x$194 , x$197 , x$195 , x$198 , x$199 , x$200 , x$201 , x$202 , x$203 , x$204 )
  37. val commuteEquivL: CoreLeftTactic

    Commute equivalence on the left CommuteEquivLeft.

    Commute equivalence on the left CommuteEquivLeft.

    q<->p, G |-  D
    -------------- (<->cL)
    p<->q, G |-  D
    Annotations
    @Tactic( x$601 , x$605 , x$602 , x$603 , x$604 , x$606 , x$607 , x$608 , x$609 , x$610 , x$611 , x$612 )
  38. val commuteEquivR: CoreRightTactic

    Commute equivalence on the right CommuteEquivRight.

    Commute equivalence on the right CommuteEquivRight.

    G |- q<->p, D
    ------------- (<->cR)
    G |- p<->q, D
    Annotations
    @Tactic( x$205 , x$209 , x$206 , x$207 , x$208 , x$210 , x$211 , x$212 , x$213 , x$214 , x$215 , x$216 )
  39. def cut(f: 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).

    Use:          Show:
    G, c |- D     G |- D, c
    ----------------------- (cut)
            G |- D
    Annotations
    @Tactic( x$436 , x$437 , x$438 , x$433 , x$434 , x$439 , x$440 , x$441 , x$442 , x$443 , x$435 , x$444 )
  40. def cutL(f: Formula): DependentPositionWithAppliedInputTactic

    cut a formula in in place of pos on the left to prove its implication on the second branch and assume it on the first.

    cut a formula in in place of pos on the left to prove its implication on the second branch and assume it on the first. (CutLeft).

    c, G |- D    G |- D, p->c
    ------------------------- (Cut Left)
           p, G |- D
    Annotations
    @Tactic( x$460 , x$461 , x$462 , x$457 , x$458 , x$463 , x$464 , x$465 , x$466 , x$467 , x$459 , x$468 )
  41. def cutLR(f: Formula): DependentPositionWithAppliedInputTactic

    cut a formula in in place of pos to prove its implication on the second branch and assume it on the first (whether pos is left or right).

    cut a formula in in place of pos to prove its implication on the second branch and assume it on the first (whether pos is left or right). (CutLeft or CutRight).

    c, G |- D    G |- D, p->c
    ------------------------- (Cut Left at antecedent<0)
           p, G |- D
    G |- c, D    G |- c->p, D
    ------------------------- (Cut right at succedent>0)
           G |- p, D
    Annotations
    @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
  42. def cutR(f: Formula): DependentPositionWithAppliedInputTactic

    cut a formula in in place of pos on the right to prove its implication on the second branch and assume it on the first.

    cut a formula in in place of pos on the right to prove its implication on the second branch and assume it on the first. (CutRight).

    G |- c, D    G |- c->p, D
    ------------------------- (Cut right)
           G |- p, D
    Annotations
    @Tactic( x$448 , x$449 , x$450 , x$445 , x$446 , x$451 , x$452 , x$453 , x$454 , x$455 , x$447 , x$456 )
  43. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  44. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  45. val equivL: DependentPositionTactic

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

    Annotations
    @Tactic( x$397 , x$400 , x$401 , x$398 , x$399 , x$402 , x$403 , x$404 , x$405 , x$406 , x$407 , x$408 )
  46. val equivLRule: CoreLeftTactic
    Annotations
    @Tactic( x$409 , x$412 , x$413 , x$410 , x$411 , x$414 , x$415 , x$416 , x$417 , x$418 , x$419 , x$420 )
  47. val equivR: DependentPositionTactic

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

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

    Annotations
    @Tactic( x$61 , x$64 , x$65 , x$62 , x$63 , x$66 , x$67 , x$68 , x$69 , x$70 , x$71 , x$72 )
  48. val equivRRule: CoreRightTactic
    Annotations
    @Tactic( x$421 , x$424 , x$425 , x$422 , x$423 , x$426 , x$427 , x$428 , x$429 , x$430 , x$431 , x$432 )
  49. val equivifyR: CoreRightTactic

    Turn implication a->b on the right into an equivalence a<->b, which is useful to prove by CE etc.

    Turn implication a->b on the right into an equivalence a<->b, which is useful to prove by CE etc. (EquivifyRight).

    G |- a<->b, D
    -------------
    G |- a->b,  D
    Annotations
    @Tactic( x$181 , x$185 , x$182 , x$183 , x$184 , x$186 , x$187 , x$188 , x$189 , x$190 , x$191 , x$192 )
  50. val exchangeL: BuiltInTwoPositionTactic

    Exchange left rule reorders antecedent.

    Exchange left rule reorders antecedent.

    q, p, G |- D
    ------------- (Exchange left)
    p, q, G |- D
    Annotations
    @Tactic( x$289 , x$293 , x$290 , x$291 , x$292 , x$294 , x$295 , x$296 , x$297 , x$298 , x$299 , x$300 )
  51. val exchangeR: BuiltInTwoPositionTactic

    Exchange right rule reorders succedent.

    Exchange right rule reorders succedent.

    G |- q, p, D
    ------------- (Exchange right)
    G |- p, q, D
    Annotations
    @Tactic( x$337 , x$341 , x$338 , x$339 , x$340 , x$342 , x$343 , x$344 , x$345 , x$346 , x$347 , x$348 )
  52. val existsL: BuiltInPositionTactic

    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.

              p(x), G |- D
    ------------------------ (Skolemize) provided x not in G,D
    \exists x p(x), G |- D
    Annotations
    @Tactic( x$265 , x$268 , x$269 , x$266 , x$267 , x$270 , x$271 , x$272 , x$273 , x$274 , x$275 , x$276 )
  53. def existsLi(t: Term, x: Option[Variable]): DependentPositionWithAppliedInputTactic
    Annotations
    @Tactic( x$517 , x$522 , x$523 , x$519 , x$520 , x$524 , x$525 , x$521 , x$526 , x$527 , x$518 , x$528 )
  54. def existsR(e: Term): BuiltInPositionTactic
  55. def existsR(e: Option[Term]): DependentPositionWithAppliedInputTactic

    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

    Annotations
    @Tactic( x$529 , x$533 , x$534 , x$531 , x$532 , x$535 , x$536 , x$537 , x$538 , x$539 , x$530 , x$540 )
  56. def existsR(x: Variable, inst: Term): BuiltInPositionTactic

    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.

    G |- p(inst), D
    ----------------------- ∃R
    G |- \exists x p(x), D
  57. val existsR: DependentPositionTactic

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

  58. def existsRPos(instPos: Position): DependentPositionTactic

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

  59. def existsRmon(q: Formula): DependentPositionWithAppliedInputTactic

    Existential monotonicity in succedent: replace p(x) with a characteristic property q(x).

    Existential monotonicity in succedent: replace p(x) with a characteristic property q(x).

    Use:                      Show:
    G |- \exists x q(x), D    G, q(x) |- p(x), D
    -------------------------------------------- M∃R
    G |- \exists x p(x), D
    Annotations
    @Tactic( x$541 , x$545 , x$546 , x$543 , x$544 , x$547 , x$548 , x$549 , x$550 , x$551 , x$542 , x$552 )
  60. val expandAll: BuiltInTactic

    Expands all special functions (abs/min/max).

  61. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  62. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  63. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  64. val hide: BuiltInPositionTactic

    Hide/weaken whether left or right

    Hide/weaken whether left or right

    Annotations
    @Tactic( x$133 , x$137 , x$134 , x$135 , x$136 , x$138 , x$139 , x$140 , x$141 , x$142 , x$143 , x$144 )
  65. val hideL: CoreLeftTactic

    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)

    Annotations
    @Tactic( x$25 , x$29 , x$26 , x$27 , x$28 , x$30 , x$31 , x$32 , x$33 , x$34 , x$35 , x$36 )
  66. val hideR: CoreRightTactic

    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)

    Annotations
    @Tactic( x$49 , x$53 , x$50 , x$51 , x$52 , x$54 , x$55 , x$56 , x$57 , x$58 , x$59 , x$60 )
  67. val id: BuiltInTactic

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

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

           *
    ------------------ (id)
      p, G |- p, D
    Annotations
    @Tactic( x$16 , x$15 , x$17 , x$13 , x$14 , x$18 , x$19 , x$20 , x$21 , x$22 , x$23 , x$24 )
  68. val idx: DependentTactic
    Annotations
    @Tactic( x$555 , x$556 , x$557 , x$553 , x$554 , x$558 , x$559 , x$560 , x$561 , x$562 , x$563 , x$564 )
  69. val implyL: DependentPositionTactic

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

    Annotations
    @Tactic( x$253 , x$256 , x$257 , x$254 , x$255 , x$258 , x$259 , x$260 , x$261 , x$262 , x$263 , x$264 )
  70. val implyLRule: CoreLeftTactic
    Annotations
    @Tactic( x$385 , x$388 , x$389 , x$386 , x$387 , x$390 , x$391 , x$392 , x$393 , x$394 , x$395 , x$396 )
  71. val implyR: CoreRightTactic

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

    Annotations
    @Tactic( x$1 , x$4 , x$5 , x$2 , x$3 , x$6 , x$7 , x$8 , x$9 , x$10 , x$11 , x$12 )
  72. def implyRi(keep: Boolean = false): BuiltInTwoPositionTactic

    Inverse of implyR.

    Inverse of implyR.

      G, G' |- D, D', a -> b
    -------------------------
      G, a, G' |- D, b, D'
  73. val implyRi: AppliedBuiltinTwoPositionTactic
  74. val implyRiX: BuiltInTwoPositionTactic

    eXternal wrapper for implyRi

    eXternal wrapper for implyRi

    Annotations
    @Tactic( "implyRi" , "implyRi" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
  75. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  76. def label(s: String): InputTactic

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

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

    Annotations
    @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
    See also

    Idioms.<()

    sublabel()

    BelleLabels

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

    Idioms.<()

    sublabel()

    BelleLabels

  78. 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
  79. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  80. val notL: CoreLeftTactic

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

    Annotations
    @Tactic( x$109 , x$112 , x$113 , x$110 , x$111 , x$114 , x$115 , x$116 , x$117 , x$118 , x$119 , x$120 )
  81. val notR: CoreRightTactic

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

    Annotations
    @Tactic( x$97 , x$100 , x$101 , x$98 , x$99 , x$102 , x$103 , x$104 , x$105 , x$106 , x$107 , x$108 )
  82. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  83. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  84. val orL: DependentPositionTactic

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

    Annotations
    @Tactic( x$37 , x$40 , x$41 , x$38 , x$39 , x$42 , x$43 , x$44 , x$45 , x$46 , x$47 , x$48 )
  85. val orLRule: CoreLeftTactic
    Annotations
    @Tactic( x$373 , x$376 , x$377 , x$374 , x$375 , x$378 , x$379 , x$380 , x$381 , x$382 , x$383 , x$384 )
  86. val orR: CoreRightTactic

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

    Annotations
    @Tactic( x$145 , x$148 , x$149 , x$146 , x$147 , x$150 , x$151 , x$152 , x$153 , x$154 , x$155 , x$156 )
  87. def orRi(keepLeft: Boolean): BuiltInTwoPositionTactic

    Inverse of orR.

    Inverse of orR.

      G |- D, D', D'', a | b
    -------------------------
      G |- D, a, D', b, D''
  88. val orRi: AppliedBuiltinTwoPositionTactic
  89. 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()

  90. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  91. def toString(): String
    Definition Classes
    AnyRef → Any
  92. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  93. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  94. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped