arnold beckmann's pages

Corrected Upper Bounds for Free-Cut Elimination

File: PDF-File

Author: Arnold Beckmann and Sam Buss
Title: Corrected Upper Bounds for Free-Cut Elimination
Journal: TCS 2011, 412(39): 5433-5445
Year: 2011
Pages: 13
DOI: 10.1016/j.tcs.2011.05.053

Abstract: The paper corrects earlier upper bounds on the size of free-cut elimination. Free-cut elimination allows cut elimination to be carried out in the presence of non-logical axioms. The correction requires that the notion of a free-cut be modified so that a cut formula is anchored provided that all of its introductions are anchored, instead of only requiring that one of its introductions is anchored. With the correction, the originally proved size upper bounds remain unchanged. These results also apply to partial cut elimination. We also apply these bounds to elimination of cuts in propositional logic.
If the non-logical inferences are closed under cut and infer only atomic formulas, then all cuts can be eliminated. This generalizes earlier results of Takeuti and of Negri and van Plato.

websites: Arnold Beckmann 2018-04-07 Valid HTML 4.01! Valid CSS!