o

gapt.cutintro

proveWithPi2Cut

object proveWithPi2Cut

Constructs a proof for a given schematic Pi2-grammar if a cut formula exists

Source
proveWithPi2Cut.scala
Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. proveWithPi2Cut
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

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 apply(endSequent: Sequent[Formula], seHs: Pi2SeHs, nameOfExistentialVariable: Var = fov"yCut", nameOfUniversalVariable: Var = fov"xCut"): Option[LKProof]

    Constructs a proof for a given schematic Pi2-grammar if a cut formula exists

    Constructs a proof for a given schematic Pi2-grammar if a cut formula exists

    endSequent

    A provable Sequent for which the method builds a proof with Pi2-cut

    seHs

    The given schematic Pi2-grammar

    nameOfExistentialVariable

    The user can name the existential variable of the cut formula. (Default = xCut; In case the name is already taken the method looks for a similar name)

    nameOfUniversalVariable

    The user can name the universal variable of the cut formula. (Default = yCut; In case the name is already taken the method looks for a similar name)

    returns

    Optiontype that contains a proof with Pi2-cut if a Pi2-cut formula exists

  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
  7. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  8. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  9. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  10. def giveProof(cutFormulaWithoutQuantifiers: Formula, seHs: Pi2SeHs, endSequent: Sequent[Formula], nameOfExVa: Var, nameOfUnVa: Var): Option[LKProof]

    The construction of the proof itself

    The construction of the proof itself

    cutFormulaWithoutQuantifiers

    The quantifier-free cut formula that corresponds to the schematic Pi2-grammar

    seHs

    The given schematic Pi2-grammar

    endSequent

    A provable Sequent for which the method builds a proof with Pi2-cut

    nameOfExVa

    Name of the existential variable of the cut-formula

    nameOfUnVa

    Name of the universal variable of the cut-formula

    returns

    Optiontype that contains a proof with Pi2-cut

  11. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  12. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  13. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  15. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  16. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  17. def toString(): String
    Definition Classes
    AnyRef → Any
  18. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  19. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  20. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

Inherited from AnyRef

Inherited from Any

Ungrouped