No Cover Image

Journal article 943 views

Corrected upper bounds for free-cut elimination

Arnold Beckmann Orcid Logo, Samuel R Buss

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

Swansea University Author: Arnold Beckmann Orcid Logo

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

Check full text

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....

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!
first_indexed 2013-07-23T11:58:44Z
last_indexed 2018-02-09T04:35:55Z
id cronfa7577
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2015-06-30T20:36:29.3446015</datestamp><bib-version>v2</bib-version><id>7577</id><entry>2012-02-23</entry><title>Corrected upper bounds for free-cut elimination</title><swanseaauthors><author><sid>1439ebd690110a50a797b7ec78cca600</sid><ORCID>0000-0001-7958-5790</ORCID><firstname>Arnold</firstname><surname>Beckmann</surname><name>Arnold Beckmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2012-02-23</date><deptcode>SCS</deptcode><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.</abstract><type>Journal Article</type><journal>Theoretical Computer Science</journal><volume>412</volume><journalNumber>39</journalNumber><paginationStart>5433</paginationStart><paginationEnd>5445</paginationEnd><publisher>Elsevier</publisher><issnPrint>0304-3975</issnPrint><issnElectronic/><keywords/><publishedDay>15</publishedDay><publishedMonth>6</publishedMonth><publishedYear>2011</publishedYear><publishedDate>2011-06-15</publishedDate><doi>10.1016/j.tcs.2011.05.053</doi><url/><notes></notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2015-06-30T20:36:29.3446015</lastEdited><Created>2012-02-23T17:02:01.0000000</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Arnold</firstname><surname>Beckmann</surname><orcid>0000-0001-7958-5790</orcid><order>1</order></author><author><firstname>Samuel R</firstname><surname>Buss</surname><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2015-06-30T20:36:29.3446015 v2 7577 2012-02-23 Corrected upper bounds for free-cut elimination 1439ebd690110a50a797b7ec78cca600 0000-0001-7958-5790 Arnold Beckmann Arnold Beckmann true false 2012-02-23 SCS 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. Journal Article Theoretical Computer Science 412 39 5433 5445 Elsevier 0304-3975 15 6 2011 2011-06-15 10.1016/j.tcs.2011.05.053 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2015-06-30T20:36:29.3446015 2012-02-23T17:02:01.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Arnold Beckmann 0000-0001-7958-5790 1 Samuel R Buss 2
title Corrected upper bounds for free-cut elimination
spellingShingle Corrected upper bounds for free-cut elimination
Arnold Beckmann
title_short Corrected upper bounds for free-cut elimination
title_full Corrected upper bounds for free-cut elimination
title_fullStr Corrected upper bounds for free-cut elimination
title_full_unstemmed Corrected upper bounds for free-cut elimination
title_sort Corrected upper bounds for free-cut elimination
author_id_str_mv 1439ebd690110a50a797b7ec78cca600
author_id_fullname_str_mv 1439ebd690110a50a797b7ec78cca600_***_Arnold Beckmann
author Arnold Beckmann
author2 Arnold Beckmann
Samuel R Buss
format Journal article
container_title Theoretical Computer Science
container_volume 412
container_issue 39
container_start_page 5433
publishDate 2011
institution Swansea University
issn 0304-3975
doi_str_mv 10.1016/j.tcs.2011.05.053
publisher Elsevier
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 0
active_str 0
description 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.
published_date 2011-06-15T03:09:26Z
_version_ 1763749885535846400
score 11.014291

Similar Items