This book on methods of cut-elimination contains a thorough and rigorous analysis of reductive cut-elimination methods and an in-depth presentation of the recent method CERES developed by the authors. It includes a detailed complexity analysis and comparison of CERES and of reductive methods. It presents several applications of CERES—to interpolation, fast cut-elimination, generalization of proofs and to the analysis of mathematical proofs. Finally, it provides an extension of CERES to non-classical logics, in particular to finitely-valued logics and to Gödel logic.
Author(s): Alexander Leitsch, Matthias Baaz
Series: Trends in Logic 34
Publisher: Springer
Year: 2011
Language: English
Pages: 295
Tags: Mathematical Logic and Foundations; Mathematical Logic and Formal Languages
Front Matter....Pages i-vi
Preface....Pages 1-3
Introduction....Pages 5-8
Preliminaries....Pages 9-37
Complexity of Cut-Elimination....Pages 39-61
Reduction and Elimination....Pages 63-104
Cut-Elimination by Resolution....Pages 105-162
Extensions of CERES....Pages 163-173
Applications of CERES....Pages 175-227
CERES in Nonclassical Logics....Pages 229-269
Related Research....Pages 271-273
Back Matter....Pages 275-287
