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.
General
Is the information for this product incomplete, wrong or inappropriate?
Let us know about it.
Does this product have an incorrect or missing image?
Send us a new image.
Is this product missing categories?
Add more categories.
Review This Product
No reviews yet - be the first to create one!