System Documentation
The system CERES implements exactly the cut-elimination method CERES within LKDe - please be referred there if you have questions on the theoretic basics.
The work flow of the system during run-time is the following:
- Process the input file, validate the XML file against a specification in form of a DTD and build up the internal representation of the input LKDe-proof φ as a data structure.
- Verify the correctness of φ according to the definition of LKDe.
- Skolemization of the proof on demand (after regularization).
- Compute the characteristic clause set CL(φ) of φ.
- Build the proof projection schemes for every clause in CL(φ).
- Generate an input file for the automated theorem prover Otter containing CL(φ) and the axiom set and execute Otter.
- Process the output file of Otter and transform the refutation into a regular PRES-proof γ.
- Compute a combined global most general unifier of γ and apply it to γ yielding δ.
- Transform δ into an LKDe-proof ψ.
- Generate the required proof projection instances and concatenate them with ψ propagating those parts of the proof projections which are parts of the end-sequent of φ to the root, producing a proof π.
- Optionally, a Herbrand sequent S is extracted from π.
- Optionally, S can be simplified
logically oralgebraically . For the algebraic simplification, a term rewriting system must be provided. - Write the XML output file containing the produced proofs, sequents, CL(φ), and the used axiom set.
Calculi
CERES works based on the following calculi definitions:
The calculi on which CERES is operating are defined on sequents respectively clauses (i.e. atomic sequents) which are represented as sequential lists of formulas, in the sense of data structures.
Algorithms
Below you find the details of some important algorithms as they are implemented in CERES:
- Skolemization Algorithm: In order to apply the CERES algorithm it is necessary to skolemize the derivation with cuts.
- Projection Building Algorithm: Describes the way the characteristic clause set and the proof projections are built with CERES.
- Simplification Algorithm: Describes the way the extracted Herbrand sequent is simplified.
Synopsis
ceres [options] <input-file> <proof-name> <output-file>
Example
ceres --cutelim -ac -h proof.xml the-proof proof-out.xml
In this example, the CERES method will be applied to the proof "the-proof" from the file proof.xml, the atomic cut normal form and the Herbrand sequent of the atomic cut normal form will be computed and the resulting proof database will be stored in proof-out.xml.
Links
- Proof Tool is a viewer for LK/LKDe-proofs.
- HLK is a compiler to generate LK/LKDe-proofs by defining them in a higher (LK/LKDe-)language.