No Cover Image

Journal article 521 views

Corrected upper bounds for free-cut elimination / Arnold Beckmann; Samuel R Buss

Theoretical Computer Science, Volume: 412, Issue: 39, Pages: 5433 - 5445

Swansea University Author: Arnold, Beckmann

Full text not available from this repository: check for access using links below.

Abstract

Free-cut elimination allows cut elimination to be carried out in the presence of non-logical axioms. Formulas in a proof are anchored provided they originate in a non-logical axiom or non-logical inference. This paper corrects and strengthens earlier upper bounds on the size of free-cut elimination....

Full description

Published in: Theoretical Computer Science
ISSN: 0304-3975
Published: Elsevier 2011
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa7577
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: Free-cut elimination allows cut elimination to be carried out in the presence of non-logical axioms. Formulas in a proof are anchored provided they originate in a non-logical axiom or non-logical inference. This paper corrects and strengthens earlier upper bounds on the size of free-cut elimination. 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 extends earlier results of Takeuti and of Negri and von Plato.
College: College of Science
Issue: 39
Start Page: 5433
End Page: 5445