Methods of Cut-Elimination

AvMatthias Baaz,Alexander Leitsch

Inbunden, Engelska, 2011

Del i serien Trends in Logic

1 102 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Fler format och utgåvor

Häftad

1 102 kr

Beskrivning

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.

Produktinformation

Utgivningsdatum:2011-01-17
Mått:155 x 235 x 27 mm
Vikt:578 g
Format:Inbunden
Språk:Engelska
Serie:Trends in Logic
Antal sidor:290
Upplaga:2011
Förlag:Springer
ISBN:9789400703193

Utforska kategorier

Mer om författaren

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.

Innehållsförteckning

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.

Mer från samma författare

Kurt Gödel and the Foundations of Mathematics

Matthias Baaz, Christos H. Papadimitriou, Hilary W. Putnam, Dana S. Scott, Charles L. Harper, Jr

Inbunden, 2011

1 992 kr

Kurt Gödel and the Foundations of Mathematics

Matthias Baaz, Christos H. Papadimitriou, Hilary W. Putnam, Dana S. Scott, Charles L. Harper, Jr

Häftad, 2014

1 051 kr

Logic Colloquium '01

Jan Krajicek, Sy-David Friedman, Matthias Baaz

E-bok

1 435 kr

Logic Colloquium '01

Matthias Baaz, Sy-David Friedman, Jan Krajícek

Inbunden, 2005

980 kr

Logic Colloquium '01

Matthias Baaz, Sy-David Friedman, Jan Krajícek

Häftad, 2005

625 kr

Logic for Programming, Artificial Intelligence, and Reasoning

Matthias Baaz, Andrei Voronkov

Häftad, 2002

572 kr

Logic for Programming, Artificial Intelligence, and Reasoning

Andrei Voronkov, Matthias Baaz

E-bok

2003

739 kr

Computer Science Logic

Matthias Baaz, Johann M. Makowsky

Häftad, 2003

1 102 kr

Computer Science Logic

Johann M. Makowsky, Matthias Baaz

E-bok

2003

1 427 kr