Methods of cut-elimination

DOI10.1007/978-94-007-0320-9MaRDI QIDQ609451zbMATH OpenOpenAlexFDO

Authors Matthias Baaz, Alexander Leitsch

Publication date 30 November 2010

Published in Trends in Logic -- Studia Logica Library (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-94-007-0320-9

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)

Review text

The book summarizes work by the authors and their collaborators on a new method of normalization of proofs called cut elimination by resolution (CERES). A clause \(p\vee q\vee\neg r\vee\neg s\) looks in their notation as \(r,s\vdash p,q\). CERES is applicable to prrofs of \textit{Skolemized} sequents in the classical first-order logic containing no weakening rules (so that even redundant formulas are carried out to the axioms). Each axiom \(S=X,A\vdash A,Y\) in a given derivation \(\phi\) is assigned a clause \(X',A'\vdash A,Y'\) consisting of all formulas in \(S\) traceable to cut formulas. The whole derivation \(\phi\) is assigned a characteristic clause term \(\Theta(\phi)\) which is a \((\&,\vee)\)-combination of the clauses assigned to the axioms. \(\Theta(\phi)\) is polynomial in the size of \(\phi\), but the result \(Cl(\phi)\) of transforming \(\Theta(\phi)\) into a conjunction of clauses may be exponential. Three results at the background of CERES are: {\parindent5mm \begin{itemize}\item[1.] The (universal closure) of \(Cl(\phi)\) is unsatisfiable. \item[2.] For each clause \(C\in Cl(\phi)\) the result of ``adding (i.e. forming a disjunction) a substitution instance of \(C\) to each sequent in \(\phi\) is a cut-free derivation. \item[3.] Any resolution derivation of a contradiction from \(Cl(\phi)\) results (via 1 and 2) in a derivation (of the same endsequent as in \(\phi\)) containing cuts only over atomic formulas. \end{itemize}} The remaining cuts can be eliminated in a standard way with at most exponential blow-up, but their presence is not an obstacle to most applications of cut elimination including interpolation. The speed-up by CERES over the standard methods of cut elimination is possible for example when \(Cl(\phi)\) belongs to one of the classes efficiently decided by resolution. Several such useful classes are described. Other potential applications concern proof-mining, i.e., analysis of mathematical proofs by extracting additional information and generalization. Extensions of CERES to non-classical logics is restricted by the necessity of Skolemization. One positive example in this book concerns many-valued logics with (what the authors call) distributive quantifiers.

Recommendations

Cited in

(40)

This page was built for publication: Methods of cut-elimination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q609451)