No Cover Image

Journal article 1138 views

Uniform Proof Complexity

A Beckmann, Arnold Beckmann Orcid Logo

Journal of Logic and Computation, Volume: 15, Issue: 4, Pages: 433 - 446

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.1093/logcom/exi035

Abstract

We define the notion of the uniform reduct of a propositional proof system as the set of those bounded formulas in the language of Peano Arithmetic which have polynomial size proofs under the Paris-Wilkie-translation. With respect to the arithmetic complexity of uniform reducts, we show that uniform...

Full description

Published in: Journal of Logic and Computation
ISSN: 0955-792X 1465-363X
Published: 2005
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa1702
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2013-07-23T11:48:09Z
last_indexed 2018-02-09T04:29:12Z
id cronfa1702
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2013-10-17T11:47:49.8727947</datestamp><bib-version>v2</bib-version><id>1702</id><entry>2011-10-01</entry><title>Uniform Proof Complexity</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>2011-10-01</date><deptcode>SCS</deptcode><abstract>We define the notion of the uniform reduct of a propositional proof system as the set of those bounded formulas in the language of Peano Arithmetic which have polynomial size proofs under the Paris-Wilkie-translation. With respect to the arithmetic complexity of uniform reducts, we show that uniform reducts are \Pi^0_1-hard and obviously in \Sigma^0_2. We also show under certain regularity conditions that each uniform reduct is closed under bounded generalisation; that in the case the language includes a symbol for exponentiation, a uniform reduct is closed under modus ponens if and only if it already contains all true bounded formulas; and that each uniform reduct contains all true \Pi^b_1(\alpha)-formulas.</abstract><type>Journal Article</type><journal>Journal of Logic and Computation</journal><volume>15</volume><journalNumber>4</journalNumber><paginationStart>433</paginationStart><paginationEnd>446</paginationEnd><publisher/><placeOfPublication/><issnPrint>0955-792X</issnPrint><issnElectronic>1465-363X</issnElectronic><keywords/><publishedDay>4</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2005</publishedYear><publishedDate>2005-08-04</publishedDate><doi>10.1093/logcom/exi035</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2013-10-17T11:47:49.8727947</lastEdited><Created>2011-10-01T00:00:00.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>A</firstname><surname>Beckmann</surname><order>1</order></author><author><firstname>Arnold</firstname><surname>Beckmann</surname><orcid>0000-0001-7958-5790</orcid><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2013-10-17T11:47:49.8727947 v2 1702 2011-10-01 Uniform Proof Complexity 1439ebd690110a50a797b7ec78cca600 0000-0001-7958-5790 Arnold Beckmann Arnold Beckmann true false 2011-10-01 SCS We define the notion of the uniform reduct of a propositional proof system as the set of those bounded formulas in the language of Peano Arithmetic which have polynomial size proofs under the Paris-Wilkie-translation. With respect to the arithmetic complexity of uniform reducts, we show that uniform reducts are \Pi^0_1-hard and obviously in \Sigma^0_2. We also show under certain regularity conditions that each uniform reduct is closed under bounded generalisation; that in the case the language includes a symbol for exponentiation, a uniform reduct is closed under modus ponens if and only if it already contains all true bounded formulas; and that each uniform reduct contains all true \Pi^b_1(\alpha)-formulas. Journal Article Journal of Logic and Computation 15 4 433 446 0955-792X 1465-363X 4 8 2005 2005-08-04 10.1093/logcom/exi035 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2013-10-17T11:47:49.8727947 2011-10-01T00:00:00.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science A Beckmann 1 Arnold Beckmann 0000-0001-7958-5790 2
title Uniform Proof Complexity
spellingShingle Uniform Proof Complexity
Arnold Beckmann
title_short Uniform Proof Complexity
title_full Uniform Proof Complexity
title_fullStr Uniform Proof Complexity
title_full_unstemmed Uniform Proof Complexity
title_sort Uniform Proof Complexity
author_id_str_mv 1439ebd690110a50a797b7ec78cca600
author_id_fullname_str_mv 1439ebd690110a50a797b7ec78cca600_***_Arnold Beckmann
author Arnold Beckmann
author2 A Beckmann
Arnold Beckmann
format Journal article
container_title Journal of Logic and Computation
container_volume 15
container_issue 4
container_start_page 433
publishDate 2005
institution Swansea University
issn 0955-792X
1465-363X
doi_str_mv 10.1093/logcom/exi035
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 We define the notion of the uniform reduct of a propositional proof system as the set of those bounded formulas in the language of Peano Arithmetic which have polynomial size proofs under the Paris-Wilkie-translation. With respect to the arithmetic complexity of uniform reducts, we show that uniform reducts are \Pi^0_1-hard and obviously in \Sigma^0_2. We also show under certain regularity conditions that each uniform reduct is closed under bounded generalisation; that in the case the language includes a symbol for exponentiation, a uniform reduct is closed under modus ponens if and only if it already contains all true bounded formulas; and that each uniform reduct contains all true \Pi^b_1(\alpha)-formulas.
published_date 2005-08-04T03:04:30Z
_version_ 1763749575771815936
score 10.997933

Similar Items