Cut-elimination: syntax and semantics (Q2259012)

This article concerns the cut-elimination by resolution (CERES) method for first-order logic [\textit{M. Baaz} et al., Lect. Notes Comput. Sci. 3452, 481--495 (2005; Zbl 1108.03305)]. Compared with reductive cut-elimination (e.g.\ Gentzen-/Schütte-/Tait-style) which can be viewed as sequences of local reductions, CERES operates globally on LK-proofs. The method first converts the ancestors of cut-formulas into an unsatisfiable formula R (the \textit{characteristic clause set}), and then a resolution refutation of R into an LK-proof with atomic cuts. As well as providing a concise overview of CERES, the authors extend the method to incorporate semantically-defined generalisations of the cut rule. The new rules (called \textit{deletions}) have the form \[ \frac {\Gamma_1 , \Delta_1 \quad \dotsm \quad \Gamma_n, \Delta_n} {\Gamma_1, \dotsc , \Gamma_n} \] where \(\bigwedge_{i} (\bigvee \Delta_i)\) is unsatisfiable. The authors prove that CERES provides a procedure for uniformly eliminating deletions. This further differentiates CERES from reductive cut-elimination: there cannot exist a uniform procedure for the latter as it would yield a decision procedure for first-order validity.