No Cover Image

Book chapter 1126 views

Characterising definable search problems in bounded arithmetic via proof notations

Arnold Beckmann Orcid Logo, Samuel R Buss

Ways of Proof Theory, Volume: 2, Pages: 65 - 134

Swansea University Author: Arnold Beckmann Orcid Logo

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

DOI (Published version): 10.1515/9783110324907.65

Abstract

The complexity class of $\Pi^p_k$-Polynomial Local Search (PLS) problems with $\Pi^p_\ell$-goal is introduced, and is used to give new characterisations of definable search problems in fragments of Bounded Arithmetic. The characterisations are established via notations for propositional proofs obtai...

Full description

Published in: Ways of Proof Theory
Published: Berlin De Gruyter 2010
Online Access: http://www.degruyter.com/view/books/9783110324907/9783110324907.65/9783110324907.65.xml
URI: https://cronfa.swan.ac.uk/Record/cronfa8149
first_indexed 2013-11-06T02:45:07Z
last_indexed 2018-02-09T04:37:01Z
id cronfa8149
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2015-06-30T20:36:55.0537311</datestamp><bib-version>v2</bib-version><id>8149</id><entry>2012-02-22</entry><title>Characterising definable search problems in bounded arithmetic via proof notations</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-22</date><deptcode>MACS</deptcode><abstract>The complexity class of $\Pi^p_k$-Polynomial Local Search (PLS) problems with $\Pi^p_\ell$-goal is introduced, and is used to give new characterisations of definable search problems in fragments of Bounded Arithmetic. The characterisations are established via notations for propositional proofs obtained by translating Bounded Arithmetic proofs using the Paris-Wilkie-translation. For $\ell\le k$, the $\Sigma^b_{\ell+1}$-definable search problems of $T^{k+1}_2$ are exactly characterised by $\Pi^p_k$-PLS problems with $\Pi^p_\ell$-goals. These $\Pi_p_k$-PLS problems can be defined in a weak base theory such as $S^1_2$, and proved to be total in $T^{k+1}_2$. Furthermore, the $\Pi^p_k$-PLS definitions can be Skolemised with simple polynomial time functions. The Skolemised $\Pi^p_k$-PLS definitions give rise to a new $\forall\Sigma^b_1(\alpha)$ principle conjectured to separate $\T^k_2(\alpha)$ from $T^{k+1}_2(\alpha)$.</abstract><type>Book chapter</type><journal>Ways of Proof Theory</journal><volume>2</volume><paginationStart>65</paginationStart><paginationEnd>134</paginationEnd><publisher>De Gruyter</publisher><placeOfPublication>Berlin</placeOfPublication><issnPrint/><issnElectronic/><keywords/><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2010</publishedYear><publishedDate>2010-12-31</publishedDate><doi>10.1515/9783110324907.65</doi><url>http://www.degruyter.com/view/books/9783110324907/9783110324907.65/9783110324907.65.xml</url><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2015-06-30T20:36:55.0537311</lastEdited><Created>2012-02-22T13:37:08.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:55.0537311 v2 8149 2012-02-22 Characterising definable search problems in bounded arithmetic via proof notations 1439ebd690110a50a797b7ec78cca600 0000-0001-7958-5790 Arnold Beckmann Arnold Beckmann true false 2012-02-22 MACS The complexity class of $\Pi^p_k$-Polynomial Local Search (PLS) problems with $\Pi^p_\ell$-goal is introduced, and is used to give new characterisations of definable search problems in fragments of Bounded Arithmetic. The characterisations are established via notations for propositional proofs obtained by translating Bounded Arithmetic proofs using the Paris-Wilkie-translation. For $\ell\le k$, the $\Sigma^b_{\ell+1}$-definable search problems of $T^{k+1}_2$ are exactly characterised by $\Pi^p_k$-PLS problems with $\Pi^p_\ell$-goals. These $\Pi_p_k$-PLS problems can be defined in a weak base theory such as $S^1_2$, and proved to be total in $T^{k+1}_2$. Furthermore, the $\Pi^p_k$-PLS definitions can be Skolemised with simple polynomial time functions. The Skolemised $\Pi^p_k$-PLS definitions give rise to a new $\forall\Sigma^b_1(\alpha)$ principle conjectured to separate $\T^k_2(\alpha)$ from $T^{k+1}_2(\alpha)$. Book chapter Ways of Proof Theory 2 65 134 De Gruyter Berlin 31 12 2010 2010-12-31 10.1515/9783110324907.65 http://www.degruyter.com/view/books/9783110324907/9783110324907.65/9783110324907.65.xml COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2015-06-30T20:36:55.0537311 2012-02-22T13:37:08.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 Characterising definable search problems in bounded arithmetic via proof notations
spellingShingle Characterising definable search problems in bounded arithmetic via proof notations
Arnold Beckmann
title_short Characterising definable search problems in bounded arithmetic via proof notations
title_full Characterising definable search problems in bounded arithmetic via proof notations
title_fullStr Characterising definable search problems in bounded arithmetic via proof notations
title_full_unstemmed Characterising definable search problems in bounded arithmetic via proof notations
title_sort Characterising definable search problems in bounded arithmetic via proof notations
author_id_str_mv 1439ebd690110a50a797b7ec78cca600
author_id_fullname_str_mv 1439ebd690110a50a797b7ec78cca600_***_Arnold Beckmann
author Arnold Beckmann
author2 Arnold Beckmann
Samuel R Buss
format Book chapter
container_title Ways of Proof Theory
container_volume 2
container_start_page 65
publishDate 2010
institution Swansea University
doi_str_mv 10.1515/9783110324907.65
publisher De Gruyter
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
url http://www.degruyter.com/view/books/9783110324907/9783110324907.65/9783110324907.65.xml
document_store_str 0
active_str 0
description The complexity class of $\Pi^p_k$-Polynomial Local Search (PLS) problems with $\Pi^p_\ell$-goal is introduced, and is used to give new characterisations of definable search problems in fragments of Bounded Arithmetic. The characterisations are established via notations for propositional proofs obtained by translating Bounded Arithmetic proofs using the Paris-Wilkie-translation. For $\ell\le k$, the $\Sigma^b_{\ell+1}$-definable search problems of $T^{k+1}_2$ are exactly characterised by $\Pi^p_k$-PLS problems with $\Pi^p_\ell$-goals. These $\Pi_p_k$-PLS problems can be defined in a weak base theory such as $S^1_2$, and proved to be total in $T^{k+1}_2$. Furthermore, the $\Pi^p_k$-PLS definitions can be Skolemised with simple polynomial time functions. The Skolemised $\Pi^p_k$-PLS definitions give rise to a new $\forall\Sigma^b_1(\alpha)$ principle conjectured to separate $\T^k_2(\alpha)$ from $T^{k+1}_2(\alpha)$.
published_date 2010-12-31T12:18:40Z
_version_ 1821407886329249792
score 11.139166

Similar Items