gapt
2.19.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.proofs/gapt.proofs.ceres_omega/AnalysisWithCeresOmega

AnalysisWithCeresOmega

gapt.proofs.ceres_omega.AnalysisWithCeresOmega
abstract class AnalysisWithCeresOmega

The generic template for using ceres_omega to analyze a proof. It performs the following steps:

  1. eliminate definitions (AnalysisWithCeresOmega.input_proof

  2. eliminate definitions (AnalysisWithCeresOmega.preprocessed_input_proof1

  3. expand non-atomic axioms (AnalysisWithCeresOmega.preprocessed_input_proof2)

  4. make the proof regular (AnalysisWithCeresOmega.preprocessed_input_proof)

  5. convert it to lk_sk (AnalysisWithCeresOmega.lksk_proof)

  6. compute the struct, css and projections (AnalysisWithCeresOmega.css,

AnalysisWithCeresOmega.projections, AnalysisWithCeresOmega.struct)

  1. map the css to first-order by lambda lifting and erasure of types (AnalysisWithCeresOmega.fol_css)

  2. try to find a refutation of the css (AnalysisWithCeresOmega.fol_refutation)

  3. reintroduce types (might fail because type erasure is a heuristic which is unsound in general) (no method available, included in step 11)

  4. reintroduce terms abstracted away by lambda lifting (no method available, included in step 11)

  5. construct an r_al proof from the refutation (AnalysisWithCeresOmega.ral_refutation)

  6. construct the acnf (AnalysisWithCeresOmega.acnf)

  7. construct the expansion proof (with atomic cuts) (AnalysisWithCeresOmega.expansion_proof)

  8. print statistics (AnalysisWithCeresOmega.printStatistics)

Attributes

Source
AnalysisWithCeresOmega.scala
Graph
Supertypes
class Object
trait Matchable
class Any
Known subtypes
class nTape2
object nTape2.type
class nTape3
object nTape3.type
class nTape4
class nTape5
class nTape5Arith
Show all

Members list

Value members

Abstract methods

def proofdb(): ExtendedProofDatabase

The proof database to start from.

The proof database to start from.

Attributes

Source
AnalysisWithCeresOmega.scala
def root_proof(): String

The name of the root proof to start with

The name of the root proof to start with

Attributes

Source
AnalysisWithCeresOmega.scala

Concrete methods

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

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
def timeout(): Duration

Timeout for call to theorem provers.

Timeout for call to theorem provers.

Attributes

Returns

the timeout as duration. default: 60 seconds

Source
AnalysisWithCeresOmega.scala

Concrete 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

Source
AnalysisWithCeresOmega.scala
lazy val css: Set[HOLSequent]

The characteristic sequent set of the preprocessed_input_proof.

The characteristic sequent set of the preprocessed_input_proof.

Attributes

Source
AnalysisWithCeresOmega.scala
lazy val expansion_proof: ExpansionProof

The expansion proof of the cut-free proof acnf.

The expansion proof of the cut-free proof acnf.

Attributes

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
lazy val lksk_proof: LKProof

The processed input proof converted to LKsk.

The processed input proof converted to LKsk.

Attributes

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
lazy val preprocessed_input_proof3: LKProof

The input proof preprocessing step 3: regularization

The input proof preprocessing step 3: regularization

Attributes

Source
AnalysisWithCeresOmega.scala
lazy val projections: Set[LKProof]

The set of projections of the preprocessed_input_proof.

The set of projections of the preprocessed_input_proof.

Attributes

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
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

Source
AnalysisWithCeresOmega.scala
Generated with