Talks and Poster Presentations (with Proceedings-Entry):
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),
2006-08-21; in: "ESCoR 2006 Empirically Successful Computerized Reasoning",
G. Sutcliffe, R. Schmidt, S. Schulz (ed.);
CEUR Workshop Proceedings,
Paper ID 11,
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.