Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
System Description: The Proof Transformation System CERES
verfasst von : Tsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo
Erschienen in: Automated Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 extracting a set of clauses from a proof with cuts. Any resolution refutation of this set then serves as a skeleton of an ACNF, an LK-proof with only atomic cuts.
The system
CERES
, an implementation of the CERES-method has been used successfully in analyzing nontrivial mathematical proofs (see 4).In this paper we describe the main features of the
CERES
system with special emphasis on the extraction of Herbrand sequents and simplification methods on these sequents. We demonstrate the Herbrand sequent extraction and simplification by a mathematical example.