gapt-examples
API
Generated with
gapt-examples/gapt.examples/nTape2

nTape2

gapt.examples.nTape2
See thenTape2 companion object
class nTape2 extends AnalysisWithCeresOmega

Version 2 of the higher-order n-Tape proof.

Attributes

Companion
object
Graph
Supertypes
class AnalysisWithCeresOmega
class Object
trait Matchable
class Any
Known subtypes
object nTape2.type

Members list

Value members

Concrete methods

override def printStatistics(): Unit

Attributes

Definition Classes
AnalysisWithCeresOmega
override def proofdb(): ExtendedProofDatabase

The proof database to start from.

The proof database to start from.

Attributes

Definition Classes
AnalysisWithCeresOmega
override def root_proof(): String

The name of the root proof to start with

The name of the root proof to start with

Attributes

Definition Classes
AnalysisWithCeresOmega

Inherited methods

def abstracted_constants_map: Hol2FolDefinitions

Attributes

Inherited from:
AnalysisWithCeresOmega
def collectStatistics(): (BigInt, BigInt, BigInt, BigInt, Int, Int, Int, BigInt, Int, Int, BigInt)

Attributes

Inherited from:
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

Value parameters

filename

The name of the file to export to

Attributes

Inherited from:
AnalysisWithCeresOmega
def fol_css: List[Sequent[FOLAtom]]

Attributes

Inherited from:
AnalysisWithCeresOmega
def skip_strategy(): Formula => Boolean

Determines if and which cuts should be taken into accoutn for cut-elimination. Default: propositional cuts are skipped.

Determines if and which cuts should be taken into accoutn for cut-elimination. Default: propositional cuts are skipped.

Attributes

Inherited from:
AnalysisWithCeresOmega
def thf_reproving_deep(filename: Option[String]): String

Attributes

Inherited from:
AnalysisWithCeresOmega
def timeout(): Duration

Timeout for call to theorem provers.

Timeout for call to theorem provers.

Attributes

Returns

the timeout as duration. default: 60 seconds

Inherited from:
AnalysisWithCeresOmega

Inherited fields

lazy val acnf: LKProof

The simulation of the ral_refutation on the projections i.e. an LKsk proof where cuts only work on atom formulas

The simulation of the ral_refutation on the projections i.e. an LKsk proof where cuts only work on atom formulas

Attributes

Inherited from:
AnalysisWithCeresOmega
lazy val css: Set[HOLSequent]

The characteristic sequent set of the preprocessed_input_proof.

The characteristic sequent set of the preprocessed_input_proof.

Attributes

Inherited from:
AnalysisWithCeresOmega
lazy val expansion_proof: ExpansionProof

The expansion proof of the cut-free proof acnf.

The expansion proof of the cut-free proof acnf.

Attributes

Inherited from:
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.

Attributes

Inherited from:
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)

Attributes

Inherited from:
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).

Attributes

Inherited from:
AnalysisWithCeresOmega
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)

Attributes

Inherited from:
AnalysisWithCeresOmega
lazy val lksk_proof: LKProof

The processed input proof converted to LKsk.

The processed input proof converted to LKsk.

Attributes

Inherited from:
AnalysisWithCeresOmega
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

Attributes

Inherited from:
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)

Attributes

Inherited from:
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

Attributes

Inherited from:
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

Attributes

Inherited from:
AnalysisWithCeresOmega
lazy val preprocessed_input_proof3: LKProof

The input proof preprocessing step 3: regularization

The input proof preprocessing step 3: regularization

Attributes

Inherited from:
AnalysisWithCeresOmega
lazy val projections: Set[LKProof]

The set of projections of the preprocessed_input_proof.

The set of projections of the preprocessed_input_proof.

Attributes

Inherited from:
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

Attributes

Inherited from:
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.

Attributes

Inherited from:
AnalysisWithCeresOmega
lazy val struct: Struct

The struct of the proof. It is an intermediate representation of the characteristic sequent set.

The struct of the proof. It is an intermediate representation of the characteristic sequent set.

Attributes

Inherited from:
AnalysisWithCeresOmega
Generated with