M. Baaz, S. Hetzl, A. Leitsch,Clemens Richter, H. Spohr:

"System Description: The Cut-Elimination System CERES";

Talk: FLoC'06 Workshop on Empirically Successful Computerized Reasoning (ESCoR), Seattle, USA; 2006-08-21; in: "ESCoR 2006 Empirically Successful Computerized Reasoning", G. Sutcliffe, R. Schmidt, S. Schulz (ed.); CEUR Workshop Proceedings, 192 (2006), ISSN: 1613-0073; Paper ID 11, 9 pages.

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 from a proof with cuts. Any resolution refutation of this set then

serves as a skeleton of an LK-proof with only atomic cuts.

The use of resolution and the enormous size of (formalized) mathematically

relevant proofs suggest an implementation able to handle rather complex

cut-elimination problems. In this paper we present an implementation of

CERES: the system CERES.

It already implements an improvement based on an extension of LK to the

calculus LKDe containing equality rules and rules for introduction of

definitions which makes it feasible to formalize and interpret mathematical

proofs in LK. Furthermore it increases the efficiency of the

cut-elimination method. The system CERES already performed well in

handling quite large proofs.

cut-elimination, paramodulation, proof analysis, resolution

Created from the Publication Database of the Vienna University of Technology.