TU Vienna logic.at Theory and Logic Group (E185-2)

## 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:

1. 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.
2. Verify the correctness of φ according to the definition of LKDe.
3. Skolemization of the proof on demand (after regularization).
4. Compute the characteristic clause set CL(φ) of φ.
5. Build the proof projection schemes for every clause in CL(φ).
6. Generate an input file for the automated theorem prover Otter containing CL(φ) and the axiom set and execute Otter.
7. Process the output file of Otter and transform the refutation into a regular PRES-proof γ.
8. Compute a combined global most general unifier of γ and apply it to γ yielding δ.
9. Transform δ into an LKDe-proof ψ.
10. 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 π.
11. Optionally, a Herbrand sequent S is extracted from π.
12. Optionally, S can be simplified logically or algebraically. For the algebraic simplification, a term rewriting system must be provided.
13. Write the XML output file containing the produced proofs, sequents, CL(φ), and the used axiom set.
Note that to use prover9 as resolution prover, both the prover9 and the prooftrans executables must be in the path.

### 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:

### 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.