Attributes
- Companion
- object
- Source
- CERES.scala
- Graph
-
- Supertypes
-
class Objecttrait Matchableclass Any
- Known subtypes
-
object CERES.type
Members list
Value members
Concrete methods
Applies the CERES method to a first order proof with equality. Internally this is handled by the RobinsoToLK method.
Applies the CERES method to a first order proof with equality. Internally this is handled by the RobinsoToLK method.
Value parameters
- p
-
a first-order LKProof (structural rules, cut, logical rules, equational rules but no definitions, schema,higher order) also each formula must be a FOLFormula, since the prover9 interface returns proofs from the FOL layer
Attributes
- Returns
-
an LK Proof in Atomic Cut Normal Form (ACNF) i.e. without quantified cuts
- Source
- CERES.scala
Attributes
- Source
- CERES.scala
Applies the CERES method to a first order proof with equality. Internally this is handled by the RobinsoToLK method.
Applies the CERES method to a first order proof with equality. Internally this is handled by the RobinsoToLK method.
Value parameters
- p
-
a first-order LKProof without strong quantifiers in the end-sequent (i.e. structural rules, cut, logical rules, equational rules but no definitions, schema,higher order)
- pred
-
a predicate to specify which cut formulas to eliminate (e.g. x => containsQuantifiers(x) to keep propositional cuts intact)
Attributes
- Returns
-
an LK Proof where all cuts are quantifier-free
- Source
- CERES.scala
Attributes
- Source
- CERES.scala
Applies the CERES method to a first order proof with equality. Internally this is handled by the ResolutionToLKProof method.
Applies the CERES method to a first order proof with equality. Internally this is handled by the ResolutionToLKProof method.
Value parameters
- endsequent
-
The end-sequent of the original proof
- projections
-
The projections of the original proof
- rp
-
A resolution refutation
Attributes
- Returns
-
an LK Proof in Atomic Cut Normal Form (ACNF) i.e. without quantified cuts
- Source
- CERES.scala
Computes the expansion proof of the CERES-normal form using projections and the resolution refutation.
Computes the expansion proof of the CERES-normal form using projections and the resolution refutation.
Value parameters
- p
-
a first-order LKProof without strong quantifiers in the end-sequent (i.e. structural rules, cut, logical rules, equational rules but no definitions, schema,higher order)
Attributes
- Returns
-
an expansion proof of the CERES-normal form computed from the projections and the resolution refutation
- Source
- CERES.scala
Finds the matching projection of an input clause in the set of projections.
Finds the matching projection of an input clause in the set of projections.
Value parameters
- endsequent
-
The common end-sequent of all projections.
- input_clause
-
The clause we need to project to.
- projections
-
The set of projections.
Attributes
- Returns
-
An LK proof endsequent x input_clause contained in projections
- Note
-
This method is passed to ResolutionToLKProof, which handles the simulation of the reflexivity introduction rule by itself.
- Source
- CERES.scala
Computes the partial expansion sequent of the matching projection of an input clause in the set of projections.
Computes the partial expansion sequent of the matching projection of an input clause in the set of projections.
Value parameters
- endsequent
-
The common end-sequent of all projections.
- input
-
The clause we need to project to, the expansion sequent we want to modify and a set which we do not change.
- projections
-
The set of projections.
Attributes
- Returns
-
An expansion sequent of the projection corresponding to the input clause, without the clause part (we compute the expansion trees of all formulas in the end-sequent of the projection except of the formulas corresponding to the input clause).
- Source
- CERES.scala
Deprecated methods
Computes the expansion proof of the CERES-normal form using projections and the resolution refutation.
Computes the expansion proof of the CERES-normal form using projections and the resolution refutation.
Value parameters
- p
-
a first-order LKProof without strong quantifiers in the end-sequent (i.e. structural rules, cut, logical rules, equational rules but no definitions, schema,higher order)
Attributes
- Returns
-
an expansion proof of the CERES-normal form computed from the projections and the resolution refutation
- Deprecated
-
[Since version 2.12] - Source
- CERES.scala