Methods of Cut-Elimination (eBook)

Matthias Baaz, Alexander Leitsch (Autoren)

eBook Download: PDF

2011
VI, 290 Seiten
Springer Netherlands (Verlag)
978-94-007-0320-9 (ISBN)

Infos

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.

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.

---

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"e;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"e;odel logic.

Inhalt

Contents 6
1 Preface 8
1.1 The History of This Book 8
1.2 Potential Readers of This Book 8
1.3 How to Read This Book 9
2 Introduction 11
3 Preliminaries 15
3.1 Formulas and Sequents 15
3.2 The Calculus LK 20
3.3 Unification and Resolution 30
4 Complexity of Cut-Elimination 44
4.1 Preliminaries 44
4.2 Proof Complexity and Herbrand Complexity 49
4.3 The Proof Sequence of R. Statman 56
5 Reduction and Elimination 67
5.1 Proof Reduction 67
5.2 The Hauptsatz 77
5.3 The Method of Tait and Schütte 89
5.4 Complexity of Cut-Elimination Methods 97
6 Cut-Elimination by Resolution 109
6.1 General Remarks 109
6.2 Skolemization of Proofs 110
6.3 Clause Terms 115
6.4 The Method CERES 118
6.5 The Complexity of CERES 131
6.6 Subsumption and p-Resolution 137
6.7 Canonic Resolution Refutations 143
6.8 Characteristic Terms and Cut-Reduction 150
6.9 Beyond R: Stronger Pruning Methods 161
6.10 Speed-Up Results 163
7 Extensions of CERES 167
7.1 General Extensions of Calculi 167
7.2 Equality Inference 173
7.3 Extension by Definition 176
8 Applications of CERES 178
8.1 Fast Cut-Elimination Classes 178
8.2 CERES and the Interpolation Theorem 192
8.3 Generalization of Proofs 212
8.4 CERES and Herbrand Sequent Extraction 215
8.5 Analysis of Mathematical Proofs 217
8.5.1 Proof Analysis by Cut-Elimination 217
8.5.2 The System ceres 218
8.5.3 The Tape Proof 219
8.5.4 The Lattice Proof 224
9 CERES in Nonclassical Logics 231
9.1 CERES in Finitely Valued Logics 232
9.1.1 Definitions 232
9.1.2 Skolemization 240
9.1.3 Skolemization of Proofs 240
9.1.4 CERES-m 243
9.2 CERES in Gödel Logic 252
9.2.1 First Order Gödel Logic and Hypersequents 253
9.2.2 The Method hyperCERES 257
9.2.3 Skolemization and de-Skolemization 258
9.2.4 Characteristic Hyperclauses and Reduced Proofs 261
9.2.5 Hyperclause Resolution 267
9.2.6 Projection of Hyperclauses into HG-Proofs 269
10 Related Research 272
10.1 Logical Analysis of Mathematical Proofs 272
10.2 New Developments in CERES 273
References 275
Index 282

Produkt-Details

• Erscheint lt. Verlag: 7.1.2011
• Reihe/Serie: Trends in Logic
• Reihe/Serie: Trends in Logic
• Zusatzinfo: VI, 290 p.
• Verlagsort: Dordrecht
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Theorie / Studium
• Themenwelt: Mathematik / Informatik ► Mathematik ► Allgemeines / Lexika
• Themenwelt: Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre
• Themenwelt: Mathematik / Informatik ► Mathematik ► Statistik
• Themenwelt: Technik
• Schlagworte: CERES • cut-elimination • Goedel logic • Proof Analysis • Resolution
• ISBN-10: 94-007-0320-1 / 9400703201
• ISBN-13: 978-94-007-0320-9 / 9789400703209