The Cut-Elimination System CERES
Cut-elimination is the most prominent form of proof transformation in logic. The elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathematical proofs. The cut-elimination method CERES (cut-elimination by resolution) works by constructing a set of clauses, the characteristic clause set, from a proof with cuts. Any refutation of this set (by resolution and paramodulation) then serves as a skeleton of a sequents-proof with only atomic cuts.
On this website we describe the basic cut-elimination method CERES itself as well as its extension by equality rules, definition rules and higher order logic. You can find detailed information about the system CERES and the current version available for download. Accompanying examples amplify the method and demonstrate the workflow of the system.
News - please visit our news section for the latest developments of the CERES system.