Abstract
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.
Supported by the Austrian Science Fund (project no. P22028-N13).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Andrews, P.B.: Resolution in Type Theory. J. of Symbolic LogicĀ 36, 414ā432 (1971)
Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Proof Transformation by CERES. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.Ā 4108, pp. 82ā93. Springer, Heidelberg (2006)
Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: System Description: The Cut-Elimination System CERES. In: Proc. ESCoR 2006, pp. 159ā167 (2006)
Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: CERES: An analysis of FĆ¼rstenbergās proof of the infinity of primes. Th. Co. Sci.Ā 403, 160ā175 (2008)
Baaz, M., Leitsch, A.: Cut-Elimination and Redundancy-Elimination by Resolution. Journal of Symbolic ComputationĀ 29, 149ā176 (2000)
Baaz, M., Leitsch, A.: Towards a Clausal Analysis of Cut-Elimination. Journal of Symbolic ComputationĀ 41, 381ā410 (2006)
Dunchev, T.: Simplification of Herbrand Sequents. Master Thesis (2009)
Gentzen, G.: Untersuchungen Ć¼ber das logische Schliessen. Mathematische ZeitschriftĀ 39, 176ā210, 405ā431 (1934-1935)
Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel Paleo, B.: Herbrand sequent extraction. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS (LNAI), vol.Ā 5144, pp. 462ā477. Springer, Heidelberg (2008)
Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel Paleo, B.: A Clausal Approach to Proof Analysis in Second-Order Logic. In: Logical Foundations of Computer Sci. (2009)
Woltzenlogel Paleo, B.: Herbrand Sequent Extraction. VDM-Verlag (2008)
Woltzenlogel Paleo, B.: A General Analysis of Cut-Elimination by CERes. PhD Thesis (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
Ā© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dunchev, T., Leitsch, A., Libal, T., Weller, D., Woltzenlogel Paleo, B. (2010). System Description: The Proof Transformation System CERES . In: Giesl, J., HƤhnle, R. (eds) Automated Reasoning. IJCAR 2010. Lecture Notes in Computer Science(), vol 6173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14203-1_36
Download citation
DOI: https://doi.org/10.1007/978-3-642-14203-1_36
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14202-4
Online ISBN: 978-3-642-14203-1
eBook Packages: Computer ScienceComputer Science (R0)