Methods of cut-elimination

Description

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. M.  Read more... 1. Preface -- 2. Introduction -- 3. Preliminaries -- 4. Complexity of cut-elimination -- 5. Reduction and elimination -- 6. Cut-elimination by resolution -- 7. Extensions of CERES -- 8. Applications of CERES -- 9. CERES in nonclassical logics -- 10. Related research. Contents......Page 6 1.2 Potential Readers of This Book......Page 9 1.3 How to Read This Book......Page 10 2. Introduction......Page 13 3.1 Formulas and Sequents......Page 17 3.2 The Calculus LK......Page 22 3.3 Unification and Resolution......Page 32 4.1 Preliminaries......Page 47 4.2 Proof Complexity and Herbrand Complexity......Page 52 4.3 The Proof Sequence of R. Statman......Page 59 5.1 Proof Reduction......Page 71 5.2 The Hauptsatz......Page 81 5.3 The Method of Tait and Schütte......Page 93 5.4 Complexity of Cut-Elimination Methods......Page 101 6.1 General Remarks......Page 113 6.2 Skolemization of Proofs......Page 114 6.3 Clause Terms......Page 119 6.4 The Method CERES......Page 122 6.5 The Complexity of CERES......Page 135 6.6 Subsumption and p-Resolution......Page 141 6.7 Canonic Resolution Refutations......Page 147 6.8 Characteristic Terms and Cut-Reduction......Page 154 6.9 Beyond R: Stronger Pruning Methods......Page 165 6.10 Speed-Up Results......Page 167 7.1 General Extensions of Calculi......Page 171 7.2 Equality Inference......Page 177 7.3 Extension by Definition......Page 180 8.1 Fast Cut-Elimination Classes......Page 183 8.2 CERES and the Interpolation Theorem......Page 197 8.3 Generalization of Proofs......Page 217 8.4 CERES and Herbrand Sequent Extraction......Page 220 8.5.1 Proof Analysis by Cut-Elimination......Page 222 8.5.2 The System ceres......Page 223 8.5.3 The Tape Proof......Page 224 8.5.4 The Lattice Proof......Page 229 9. CERES in Nonclassical Logics......Page 237 9.1.1 Definitions......Page 238 9.1.3 Skolemization of Proofs......Page 246 9.1.4 CERES-m......Page 249 9.2 CERES in Gödel Logic......Page 258 9.2.1 First Order Gödel Logic and Hypersequents......Page 259 9.2.2 The Method hyperCERES......Page 263 9.2.3 Skolemization and de-Skolemization......Page 264 9.2.4 Characteristic Hyperclauses and Reduced Proofs......Page 267 9.2.5 Hyperclause Resolution......Page 273 9.2.6 Projection of Hyperclauses into HG-Proofs......Page 275 10.1 Logical Analysis of Mathematical Proofs......Page 279 10.2 New Developments in CERES......Page 280 References......Page 283 Index......Page 291