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.
