Characterising definable search problems in bounded arithmetic via proof notations

Beckmann, Arnold; Buss, Samuel R

doi:10.1515/9783110324907.65

Book chapter 1036 views

Characterising definable search problems in bounded arithmetic via proof notations

Arnold Beckmann

, Samuel R Buss

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

Swansea University Author: Arnold Beckmann

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
Tags:	Add Tag No Tags, Be the first to tag this record!

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>SCS</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>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</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 SCS 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 Computer Science COLLEGE CODE SCS 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-31T03:10:14Z
_version_	1763749935752151040
score	11.012678

Characterising definable search problems in bounded arithmetic via proof notations

Similar Items