Introduction

A characteristic feature of the famous cut-elimination method by Gentzen is the stepwise reduction of cut-complexity. In this reduction the cut formulas are decomposed w.r.t. their out-most logical operator. Moreover the cut formulas to be eliminated must be rendered main formulas of inferences by adequate proof transformations.

Despite its elegance the method of Gentzen is very costly, as it is largely independent of the inner structures of the cut formulas. These inner structures are the essence of cuts in real mathematics: mathematical arguments are typically based on explicit definitions, e.g. differentials, integrals etc. Therefore it is useful to concentrate on cut-elimination procedures which eliminate cuts by analyzing these explicit definitions and reducing cuts from inside out.

In Baaz Leitsch 1997, (FTP97) and Baaz Leitsch 1999, (JSC) a different cut elimination method has been presented: This method characterizes cuts by sets of clauses obtained from the derivation of the cut formulas. These sets of clauses are always unsatisfiable and thus have a resolution refutation. Any such refutation serves as skeleton of an LK-proof with only atomic cuts.

CRes is a system which takes as input a proof P with skolemized end-sequent in Gentzen sequent calculus and produces a sequent calculus proof S with only atomic cuts. The output is in LaTeX-format complete with notations and definitions. Clearly it is easy to lift this restriction by skolemizing the proof as a pre-processing step and re-skolemize the final proof.

The System

The components of CRes V0.5 are written in SICStus Prolog. The main task is to compute an unsatisfiable set of clauses C characterizing the cut formulas. On this set of clauses a resolution theorem prover (the present version uses SPASS V0.86 as prover, but any refutational theorem prover can be used.} is invoked. The resolution refutation R is re-translated to sequent notation and a ground-projection is computed.

For each clause c in C the system generates a projection P_c---deriving the respective clause with additional side-formulas---out of the original proof P. In the last step, R is extended with the projections P_{c} to obtain the final proof S. The system CRes, System Description has been presented at CADE-16, Trento. The latest version will be presented at the workshop on proof theory, Collegium Logicum 1999: Proof Theory, Vienna, November 18, 19, 1999.

I'm not completly satisfied with the latest version (V0.3) of CRes. E.g. I don't know its behaviour on real-world proofs, I don't know its time-complexity; no nice user-interface e.g. a WWW-interface, exists. As soon as the majority of these things have been accomplished, there will be a specialised webpage including source code, manual, and examples. I promise :-)

Still if you want to fool around with the SICStus source code: Source: Version 0.4 and Version 0.5 If you have any questions about the present version or any nice example proofs P, don't hesitate to contact me.

G Moser
Last modified: Mon Feb 19 14:21:26 CET 2001