Journal article 942 views
Corrected upper bounds for free-cut elimination
,
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.
DOI (Published version): 10.1016/j.tcs.2011.05.053
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....
| 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: |
Faculty of Science and Engineering |
| Issue: |
39 |
| Start Page: |
5433 |
| End Page: |
5445 |