class nTape3 extends AnalysisWithCeresOmega
Version 3 of the higher-order n-Tape proof.
- Source
- nTape3.scala
- Alphabetic
- By Inheritance
- nTape3
- AnalysisWithCeresOmega
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new nTape3()
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- def +(other: String): String
- def ->[B](y: B): (nTape3, B)
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- lazy val abstracted_constants_map: Hol2FolDefinitions
The first order export of the preprocessed characteristic sequent set (preprocessed_css), together with the map of replacing constants.
The first order export of the preprocessed characteristic sequent set (preprocessed_css), together with the map of replacing constants.
- Definition Classes
- AnalysisWithCeresOmega
- lazy val acnf: LKProof
The simulation of the ral_refutation on the projections i.e.
The simulation of the ral_refutation on the projections i.e. an LKsk proof where cuts only work on atom formulas
- Definition Classes
- AnalysisWithCeresOmega
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
- def collectStatistics(): (BigInt, BigInt, BigInt, BigInt, Int, Int, Int, BigInt, Int, Int, BigInt)
- Definition Classes
- AnalysisWithCeresOmega
- lazy val css: Set[HOLSequent]
The characteristic sequent set of the preprocessed_input_proof.
The characteristic sequent set of the preprocessed_input_proof.
- Definition Classes
- AnalysisWithCeresOmega
- def ensuring(cond: (nTape3) => Boolean, msg: => Any): nTape3
- def ensuring(cond: (nTape3) => Boolean): nTape3
- def ensuring(cond: Boolean, msg: => Any): nTape3
- def ensuring(cond: Boolean): nTape3
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- lazy val expansion_proof: ExpansionProof
The expansion proof of the cut-free proof acnf.
The expansion proof of the cut-free proof acnf.
- Definition Classes
- AnalysisWithCeresOmega
- lazy val expansion_proof_fol_deep: FOLFormula
A first-order conversion of the deep formula of the expansion_proof.
A first-order conversion of the deep formula of the expansion_proof.
- Definition Classes
- AnalysisWithCeresOmega
- def export_thf(filename: String): Unit
Exports the preprocessed characteristic sequent (preprocessed_css) set to the TPTP THF format
Exports the preprocessed characteristic sequent (preprocessed_css) set to the TPTP THF format
- filename
The name of the file to export to
- Definition Classes
- AnalysisWithCeresOmega
- lazy val fol_css: List[Sequent[FOLAtom]]
The first order export of the preprocessed characteristic sequent set (preprocessed_css), together with the map of replacing constants.
The first order export of the preprocessed characteristic sequent set (preprocessed_css), together with the map of replacing constants.
- Definition Classes
- AnalysisWithCeresOmega
- lazy val fol_refutation: ResolutionProof
The first order refutation of the first order characteristic sequent set (fol_css)
The first order refutation of the first order characteristic sequent set (fol_css)
- Definition Classes
- AnalysisWithCeresOmega
- lazy val fol_refutation_expansion_proof: ExpansionProof
The expansion proof of the first-order refutation (fol_refutation).
The expansion proof of the first-order refutation (fol_refutation).
- Definition Classes
- AnalysisWithCeresOmega
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @IntrinsicCandidate()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @IntrinsicCandidate()
- lazy val input_proof: LKProof
The input LK proof, extracted by the name root_proof from the proof database (proofdb)
The input LK proof, extracted by the name root_proof from the proof database (proofdb)
- Definition Classes
- AnalysisWithCeresOmega
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- lazy val lksk_proof: LKProof
The processed input proof converted to LKsk.
The processed input proof converted to LKsk.
- Definition Classes
- AnalysisWithCeresOmega
- 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()
- lazy val preprocessed_css: List[HOLSequent]
The characteristic sequent set (css) after removal of labels and subsumption
The characteristic sequent set (css) after removal of labels and subsumption
- Definition Classes
- AnalysisWithCeresOmega
- lazy val preprocessed_input_proof: LKProof
The input proof (TAPEPROOF) after definition elimination(preprocessed_input_proof1, expansion of logical axioms to atomic axioms (preprocessed_input_proof2) and regularization (preprocessed_input_proof3)
The input proof (TAPEPROOF) after definition elimination(preprocessed_input_proof1, expansion of logical axioms to atomic axioms (preprocessed_input_proof2) and regularization (preprocessed_input_proof3)
- Definition Classes
- AnalysisWithCeresOmega
- lazy val preprocessed_input_proof1: LKProof
The input proof (TAPEPROOF) after preprocessing step 1: definition elimination
The input proof (TAPEPROOF) after preprocessing step 1: definition elimination
- Definition Classes
- AnalysisWithCeresOmega
- lazy val preprocessed_input_proof2: LKProof
The input proof after preprocessing step 2: expansion of logical axioms to atomic axioms
The input proof after preprocessing step 2: expansion of logical axioms to atomic axioms
- Definition Classes
- AnalysisWithCeresOmega
- lazy val preprocessed_input_proof3: LKProof
The input proof preprocessing step 3: regularization
The input proof preprocessing step 3: regularization
- Definition Classes
- AnalysisWithCeresOmega
- def printStatistics(): Unit
- Definition Classes
- nTape3 → AnalysisWithCeresOmega
- def print_css_thf(): Unit
Prints the preprocessed characteristic sequent set in TPTP THF format.
Prints the preprocessed characteristic sequent set in TPTP THF format. Use export_thf to write it to a file.
- Definition Classes
- AnalysisWithCeresOmega
- lazy val projections: Set[LKProof]
The set of projections of the preprocessed_input_proof.
The set of projections of the preprocessed_input_proof.
- Definition Classes
- AnalysisWithCeresOmega
- def proofdb(): ExtendedProofDatabase
The proof database to start from.
The proof database to start from.
- Definition Classes
- nTape3 → AnalysisWithCeresOmega
- lazy val ral_refutation: ResolutionProof
The ral version of the first-order refutation (fol_refutation), with all necessary simplifications undone
The ral version of the first-order refutation (fol_refutation), with all necessary simplifications undone
- Definition Classes
- AnalysisWithCeresOmega
- lazy val reproved_deep: ResolutionProof
The proof of the deep formula of the expansion_proof.
The proof of the deep formula of the expansion_proof.
- Definition Classes
- AnalysisWithCeresOmega
- def root_proof(): String
The name of the root proof to start with
The name of the root proof to start with
- Definition Classes
- nTape3 → AnalysisWithCeresOmega
- def skip_strategy(): (Formula) => Boolean
Determines if and which cuts should be taken into accoutn for cut-elimination.
Determines if and which cuts should be taken into accoutn for cut-elimination. Default: propositional cuts are skipped.
- Definition Classes
- AnalysisWithCeresOmega
- lazy val struct: Struct
The struct of the proof.
The struct of the proof. It is an intermediate representation of the characteristic sequent set.
- Definition Classes
- AnalysisWithCeresOmega
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def thf_reproving_deep(filename: Option[String]): String
- Definition Classes
- AnalysisWithCeresOmega
- def timeout(): Duration
Timeout for call to theorem provers.
Timeout for call to theorem provers.
- returns
the timeout as duration. default: 60 seconds
- Definition Classes
- AnalysisWithCeresOmega
- 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])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
- def formatted(fmtstr: String): String
- Implicit
- This member is added by an implicit conversion from nTape3 toStringFormat[nTape3] performed by method StringFormat in scala.Predef.
- Definition Classes
- StringFormat
- Annotations
- @deprecated @inline()
- Deprecated
(Since version 2.12.16) Use
formatString.format(value)instead ofvalue.formatted(formatString), or use thef""string interpolator. In Java 15 and later,formattedresolves to the new method in String which has reversed parameters.
- def →[B](y: B): (nTape3, B)
- Implicit
- This member is added by an implicit conversion from nTape3 toArrowAssoc[nTape3] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @deprecated
- Deprecated
(Since version 2.13.0) Use
->instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.
This is the API documentation for GAPT.
The main package is gapt.