| 书目名称 | Methods of Cut-Elimination |
| 编辑 | Alexander Leitsch,Matthias Baaz |
| 视频video | |
| 概述 | 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 |
| 丛书名称 | Trends in Logic |
| 图书封面 |  |
| 描述 | .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 c |
| 出版日期 | Book 2011 |
| 关键词 | CERES; Goedel logic; cut-elimination; proof analysis; resolution |
| 版次 | 1 |
| doi | https://doi.org/10.1007/978-94-007-0320-9 |
| isbn_softcover | 978-94-007-3497-5 |
| isbn_ebook | 978-94-007-0320-9Series ISSN 1572-6126 Series E-ISSN 2212-7313 |
| issn_series | 1572-6126 |
| copyright | Springer Science+Business Media B.V. 2011 |
发表于 2025-3-21 16:18:35
