Methods of Cut-Elimination
-
- Hardcover ausgewählt
- Taschenbuch
- eBook
-
Sprache:Englisch
Fr. 138.00
inkl. gesetzl. MwSt.,
Beschreibung
Produktdetails
Einband
Gebundene Ausgabe
Erscheinungsdatum
17.01.2011
Abbildungen
VI, 290 p.
Verlag
Springer NetherlandSeitenzahl
290
Maße (L/B/H)
24.3/16.7/2.7 cm
Gewicht
578 g
Auflage
2011 edition
Sprache
Englisch
ISBN
978-94-007-0319-3
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.
Noch keine Bewertungen vorhanden
Verfassen Sie die erste Bewertung zu diesem Artikel
Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.