The Method CERES
The description of the cut-elimination method CERES cuts into the following sections:
- LK
- LKDe
- Skolemization of Proofs
- The Characteristic Clause Set
- Projection and Refutation
- CERESω
- Bibliography
This documentation is also available for download [pdf | ps].
Further Reading
Besides the publications in connection with the method CERES which are listed as references we provide the following material for download:
- Towards a Clausal Analysis of Cut-Elimination [pdf]
- Proof Transformations by Resolution - Computational Methods of Cut-Elimination [pdf | ps]
- Equational Theories in CERES [pdf | ps]
- Comparing the Complexity of Cut-Elimination Methods [pdf]
Note that some of these papers are not up to date (in the sense that they do not use the current formalisms or extensions) but still contain valuable information and details concerning the method and the system CERES.