object CutIntroduction
Ordering
- Alphabetic
- By Inheritance
Inherited
- CutIntroduction
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
Type Members
- trait BackgroundTheory extends AnyRef
- class CutIntroException extends Exception
- abstract case class InputProof extends Product with Serializable
- class NonCoveringGrammarException extends CutIntroException
- class UnprovableException extends CutIntroException
Thrown if Extended Herbrand Sequent is unprovable.
Thrown if Extended Herbrand Sequent is unprovable. In theory this does not happen. In practice it does happen if the method used for searching a proof covers a too weak theory (e.g. no equality) or is not complete.
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def apply(inputProof: InputProof, method: GrammarFindingMethod = DeltaTableMethod(), useInterpolation: Boolean = false): Option[LKProof]
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def buildProofWithCut(solStruct: SolutionStructure, prover: Prover): LKProof
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
- def compressToSolutionStructure(inputProof: InputProof, method: GrammarFindingMethod = DeltaTableMethod(), useInterpolation: Boolean = false): Option[SolutionStructure]
- def computeCanonicalSolution(sehs: SchematicExtendedHerbrandSequent): List[FOLFormula]
Computes the modified canonical solution, where instances of formulas in the end-sequent are introduced as late as possible.
- def constructLKProof(solStruct: SolutionStructure, backgroundTheory: BackgroundTheory): LKProof
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @IntrinsicCandidate()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @IntrinsicCandidate()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- val logger: Logger
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @IntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @IntrinsicCandidate()
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- object BackgroundTheory
- object InputProof extends Serializable
- object computeSolutionViaDls
This is the API documentation for GAPT.
The main package is gapt.