Overview
- First book on methods of cut-elimination
- Combines techniques and results from proof theory and automated deduction
- Thereby the book provides a completely new view on proof theoretic methods and their applications
- This specific feature makes the book interesting for researchers and graduate students in proof theory and computational logic
Part of the book series: Trends in Logic (TREN, volume 34)
Access this book
Tax calculation will be finalised at checkout
Other ways to access
Table of contents (10 chapters)
Keywords
About this book
This is the first book on cut-elimination in first-order predicate logic from an algorithmic point of view. Instead of just proving the existence of cut-free proofs, it focuses on the algorithmic methods transforming proofs with arbitrary cuts to proofs with only atomic cuts (atomic cut normal forms, so-called ACNFs). The first part investigates traditional reductive methods from the point of view of proof rewriting. Within this general framework, generalizations of Gentzen's and Sch\”utte-Tait's cut-elimination methods are defined and shown terminating with ACNFs of the original proof. Moreover, a complexity theoretic comparison of Gentzen's and Tait's methods is given.
The core of the book centers around the cut-elimination method CERES (cut elimination by resolution) developed by the authors. CERES is based on the resolution calculus and radically differs from the reductive cut-elimination methods. The book shows that CERES asymptotically outperforms all reductive methods based on Gentzen's cut-reduction rules. It obtains this result by heavy use of subsumption theorems in clause logic. Moreover, several applications of CERES are given (to interpolation, complexity analysis of cut-elimination, generalization of proofs, and to the analysis of real mathematical proofs). Lastly, the book demonstrates that CERES can be extended to nonclassical logics, in particular to finitely-valued logics and to G\"odel logic.
Authors and Affiliations
About the authors
Matthias Baaz is professor of logical foundations of computer science at the Vienna University of Technology. He obtained his Ph.D. in mathematical logic at the University of Vienna and habilitation at the Vienna University of Technology. His main field of research is proof theory in classical and nonclassical logics.
Alexander Leitsch is professor of mathematics and theoretical computer science at the Vienna University of Technology. He obtained his Ph.D. in mathematics at the University of Vienna and habilitation at the University of Linz. His research areas are automated deduction and computational proof theory.
Bibliographic Information
Book Title: Methods of Cut-Elimination
Authors: Alexander Leitsch, Matthias Baaz
Series Title: Trends in Logic
DOI: https://doi.org/10.1007/978-94-007-0320-9
Publisher: Springer Dordrecht
eBook Packages: Mathematics and Statistics, Mathematics and Statistics (R0)
Copyright Information: Springer Science+Business Media B.V. 2011
Hardcover ISBN: 978-94-007-0319-3Published: 17 January 2011
Softcover ISBN: 978-94-007-3497-5Published: 25 February 2013
eBook ISBN: 978-94-007-0320-9Published: 07 January 2011
Series ISSN: 1572-6126
Series E-ISSN: 2212-7313
Edition Number: 1
Number of Pages: VI, 290
Topics: Mathematical Logic and Foundations, Mathematical Logic and Formal Languages