System Description: The Proof Transformation System CERESReport as inadecuate

System Description: The Proof Transformation System CERES - Download this document for free, or read online. Document in PDF available to download.

* Corresponding author 1 TU WIEN - Technical University of Vienna Vienna 2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods

Abstract : Cut-elimination is the most prominent form of proof trans- formation 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 resolu- tion 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 spe- cial emphasis on the extraction of Herbrand sequents and simplification methods on these sequents. We demonstrate the Herbrand sequent ex- traction and simplification by a mathematical example.

Author: Tsvetan Dunchev - Alexander Leitsch - Tomer Libal - Daniel Weller - Bruno Woltzenlogel Paleo -



Related documents