Cut normal forms and proof complexity
type: Item
instance of: scholarly article
title: Cut normal forms and proof complexity
zbMATH Open document ID: 0940.03062
DOI: 10.1016/S0168-0072(98)00026-8
author: Matthias Baaz
author: Alexander Leitsch
published in: Annals of Pure and Applied Logic
publication date: 2000-07-24T00:00:00Z
review text: Cut-elimination in first-order logic is known to have a non-elementary complexity. The authors investigate ``reduction classes'' \(K\) for cuts [cuts over formulas \(\notin K\) can be feasibly eliminated or replaced by cut-formulas in \(K]\) and for cut-elimination [if all cut formulas are in \(K\) then all cuts can be feasibly eliminated]. For \(K=\text{NNF}\) (negative normal form: no implication, and negations are applied only to atomic formulas) every cut is easily reduced to a formula in \(K\), and hence cut-elimination for \(K\) is not feasible. For \(K=\) Prenex Normal Forms there is a quadratic transformation of a proof with arbitrary cut-formulas into a proof with cut-formulas in \(K\) sending derivable formulas into \(K\). However, elimination of new cuts introduced in this way can be non-elementary. Monotone formulas are constructed by atoms including \(\perp\) by \(\forall,\exists,\&,\vee\). The authors prove that the elimination of non-monotone cuts has non-elementary complexity in the worst case. First, all monotone cuts are proved to be quickly (almost exponentially) eliminable from proofs of quasi-monotone formulas. Then it is noticed that Statman's sequence of equational sequents with no Kalmar-elementary bound for cut-elimination can be encoded by quasi-monotone formulas. The long proof of quick cut-elimination in the paper can be simplified using two observations. Statman's sequence is encoded by Horn formulas, and pruning transformations (underlying Harrop's theorem) allow drastically ``skolemize'' monotone formulas proved from universal Horn axioms.
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F20
zbMATH DE Number: 1340820
zbMATH Keywords: cut normal forms
zbMATH Keywords: cut-elimination
zbMATH Keywords: non-monotone cuts
zbMATH Keywords: non-elementary complexity
zbMATH Keywords: equational sequents
reviewed by: G. E. Mints
MaRDI profile type: Publication
cites work: Q4304753
cites work: Q4362908
cites work: Q3882443
cites work: Lower bounds for increasing complexity of derivations after cut elimination
cites work: Q5310891
cites work: Lower Bounds on Herbrand's Theorem
cites work: Proof theory. 2nd ed
description: scientific article; zbMATH DE number 1340820