abstract class AnalysisWithCeresOmega extends AnyRef
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)
7) map the css to first-order by lambda lifting and erasure of types (AnalysisWithCeresOmega.fol_css)
8) try to find a refutation of the css (AnalysisWithCeresOmega.fol_refutation)
9) reintroduce types (might fail because type erasure is a heuristic which is unsound in general) (no method available, included in step 11)
10) reintroduce terms abstracted away by lambda lifting (no method available, included in step 11)
11) construct an r_al proof from the refutation (AnalysisWithCeresOmega.ral_refutation)
12) construct the acnf (AnalysisWithCeresOmega.acnf)
13) construct the expansion proof (with atomic cuts) (AnalysisWithCeresOmega.expansion_proof)
14) print statistics (AnalysisWithCeresOmega.printStatistics)
- Alphabetic
- By Inheritance
- AnalysisWithCeresOmega
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new AnalysisWithCeresOmega()
Abstract Value Members
- abstract def proofdb(): ExtendedProofDatabase
The proof database to start from.
- abstract def root_proof(): String
The name of the root proof to start with
Concrete Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- def +(other: String): String
- Implicit
- This member is added by an implicit conversion from AnalysisWithCeresOmega toany2stringadd[AnalysisWithCeresOmega] performed by method any2stringadd in scala.Predef.
- Definition Classes
- any2stringadd
- def ->[B](y: B): (AnalysisWithCeresOmega, B)
- Implicit
- This member is added by an implicit conversion from AnalysisWithCeresOmega toArrowAssoc[AnalysisWithCeresOmega] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @inline()
- 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.
- 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
- 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)
- lazy val css: Set[HOLSequent]
The characteristic sequent set of the preprocessed_input_proof.
- def ensuring(cond: (AnalysisWithCeresOmega) => Boolean, msg: => Any): AnalysisWithCeresOmega
- Implicit
- This member is added by an implicit conversion from AnalysisWithCeresOmega toEnsuring[AnalysisWithCeresOmega] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: (AnalysisWithCeresOmega) => Boolean): AnalysisWithCeresOmega
- Implicit
- This member is added by an implicit conversion from AnalysisWithCeresOmega toEnsuring[AnalysisWithCeresOmega] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean, msg: => Any): AnalysisWithCeresOmega
- Implicit
- This member is added by an implicit conversion from AnalysisWithCeresOmega toEnsuring[AnalysisWithCeresOmega] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean): AnalysisWithCeresOmega
- Implicit
- This member is added by an implicit conversion from AnalysisWithCeresOmega toEnsuring[AnalysisWithCeresOmega] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- 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.
- lazy val expansion_proof_fol_deep: FOLFormula
A first-order conversion of the deep formula of the expansion_proof.
- 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
- 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.
- lazy val fol_refutation: ResolutionProof
The first order refutation of the first order characteristic sequent set (fol_css)
- lazy val fol_refutation_expansion_proof: ExpansionProof
The expansion proof of the first-order refutation (fol_refutation).
- 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)
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- lazy val lksk_proof: LKProof
The processed input proof converted to LKsk.
- 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
- 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)
- lazy val preprocessed_input_proof1: LKProof
The input proof (TAPEPROOF) after preprocessing step 1: definition elimination
- lazy val preprocessed_input_proof2: LKProof
The input proof after preprocessing step 2: expansion of logical axioms to atomic axioms
- lazy val preprocessed_input_proof3: LKProof
The input proof preprocessing step 3: regularization
- def printStatistics(): Unit
- 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.
- lazy val projections: Set[LKProof]
The set of projections of the preprocessed_input_proof.
- lazy val ral_refutation: ResolutionProof
The ral version of the first-order refutation (fol_refutation), with all necessary simplifications undone
- lazy val reproved_deep: ResolutionProof
The proof of the deep formula of the expansion_proof.
- 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.
- lazy val struct: Struct
The struct of the proof.
The struct of the proof. It is an intermediate representation of the characteristic sequent set.
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def thf_reproving_deep(filename: Option[String]): String
- def timeout(): Duration
Timeout for call to theorem provers.
Timeout for call to theorem provers.
- returns
the timeout as duration. default: 60 seconds
- 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 AnalysisWithCeresOmega toStringFormat[AnalysisWithCeresOmega] 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,formatted
resolves to the new method in String which has reversed parameters.
- def →[B](y: B): (AnalysisWithCeresOmega, B)
- Implicit
- This member is added by an implicit conversion from AnalysisWithCeresOmega toArrowAssoc[AnalysisWithCeresOmega] 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.