Abstract
CERES is a method for cut-elimination in classical logic which is based on resolution. In this paper we extend CERES to CERES-m, a resolution-based method of cut-elimination in Gentzen calculi for arbitrary finitely-valued logics. Like in the classical case the core of the method is the construction of a resolution proof in finitely-valued logics. Compared to Gentzen-type cut-elimination methods the advantage of CERES-m is a twofold one: 1. it is easier to define and 2. it is computationally superior and thus more appropriate for implementations and experiments.
supported by the Austrian Science Fund (FWF) proj. no P16264-N05
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Baaz, M., Fermüller, C.: Resolution-Based Theorem Proving for Many-Valued Logics. Journal of Symbolic Computation 19(4), 353–391 (1995)
Baaz, M., Fermüller, C., Salzer, G.: Automated Deduction for Many-Valued Logics. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning 2, pp. 1356–1402. Elsevier and MIT Press (2001)
Baaz, M., Fermüller, C., Zach, R.: Elimination of Cuts in First-order Finite-valued Logics. J. Inform. Process. Cybernet (EIK) 29(6), 333–355 (1994)
Baaz, M., Leitsch, A.: Cut normal forms and proof complexity. Annals of Pure and Applied Logic 97, 127–177 (1999)
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 (to appear)
Carnielli, W.A.: Systematization of Finite Many-Valued Logics through the Method of Tableaux. Journal of Symbolic Logic 52(2), 473–493 (1987)
Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39, 405–431 (1934–1935)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baaz, M., Leitsch, A. (2005). CERES in Many-Valued Logics. In: Baader, F., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2005. Lecture Notes in Computer Science(), vol 3452. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32275-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-32275-7_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25236-8
Online ISBN: 978-3-540-32275-7
eBook Packages: Computer ScienceComputer Science (R0)