No Cover Image

Journal article 1350 views

Improved witnessing and local improvement principles for second-order bounded arithmetic

Arnold Beckmann Orcid Logo, Samuel R Buss

ACM Transactions on Computational Logic, Volume: 15, Issue: 1, Pages: 2:1 - 2:35

Swansea University Author: Arnold Beckmann Orcid Logo

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

DOI (Published version): 10.1145/2559950

Abstract

This paper concerns the second order systems U^1_2 and V^1_2 of bounded arithmetic, which have proof theoretic strengths corresponding to polynomial space and exponential time computation. We formulate improved witnessing theorems for these two theories by using S^1_2 as a base theory for proving th...

Full description

Published in: ACM Transactions on Computational Logic
Published: 2014
URI: https://cronfa.swan.ac.uk/Record/cronfa14370
first_indexed 2013-07-23T12:12:08Z
last_indexed 2019-07-17T19:59:21Z
id cronfa14370
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-07-17T15:38:07.7889743</datestamp><bib-version>v2</bib-version><id>14370</id><entry>2013-02-26</entry><title>Improved witnessing and local improvement principles for second-order bounded arithmetic</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>2013-02-26</date><deptcode>MACS</deptcode><abstract>This paper concerns the second order systems U^1_2 and V^1_2 of bounded arithmetic, which have proof theoretic strengths corresponding to polynomial space and exponential time computation. We formulate improved witnessing theorems for these two theories by using S^1_2 as a base theory for proving the correctness of the polynomial space or exponential time witnessing functions. We develop the theory of nondeterministic polynomial space computation in U^1_2 . Ko&#x142;odziejczyk, Nguyen, and Thapen have introduced local improvement properties to characterize the provably total NP functions of these second order theories. We show that the strengths of their local improvement principles over U^1_2 and V^1_2 depend primarily on the topology of the underlying graph, not the number of rounds in the local improvement games. The theory U^1_2 proves the local improvement principle for linear graphs even without restricting to logarithmically many rounds. The local improvement principle for grid graphs with only logarithmically rounds is complete for the provably total NP search problems of V^1_2 . Related results are obtained for local improvement principles with one improvement round, and for local improvement over rectangular grids.</abstract><type>Journal Article</type><journal>ACM Transactions on Computational Logic</journal><volume>15</volume><journalNumber>1</journalNumber><paginationStart>2:1</paginationStart><paginationEnd>2:35</paginationEnd><publisher/><keywords/><publishedDay>28</publishedDay><publishedMonth>2</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-02-28</publishedDate><doi>10.1145/2559950</doi><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>2019-07-17T15:38:07.7889743</lastEdited><Created>2013-02-26T10:39:43.6851048</Created><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 2019-07-17T15:38:07.7889743 v2 14370 2013-02-26 Improved witnessing and local improvement principles for second-order bounded arithmetic 1439ebd690110a50a797b7ec78cca600 0000-0001-7958-5790 Arnold Beckmann Arnold Beckmann true false 2013-02-26 MACS This paper concerns the second order systems U^1_2 and V^1_2 of bounded arithmetic, which have proof theoretic strengths corresponding to polynomial space and exponential time computation. We formulate improved witnessing theorems for these two theories by using S^1_2 as a base theory for proving the correctness of the polynomial space or exponential time witnessing functions. We develop the theory of nondeterministic polynomial space computation in U^1_2 . Kołodziejczyk, Nguyen, and Thapen have introduced local improvement properties to characterize the provably total NP functions of these second order theories. We show that the strengths of their local improvement principles over U^1_2 and V^1_2 depend primarily on the topology of the underlying graph, not the number of rounds in the local improvement games. The theory U^1_2 proves the local improvement principle for linear graphs even without restricting to logarithmically many rounds. The local improvement principle for grid graphs with only logarithmically rounds is complete for the provably total NP search problems of V^1_2 . Related results are obtained for local improvement principles with one improvement round, and for local improvement over rectangular grids. Journal Article ACM Transactions on Computational Logic 15 1 2:1 2:35 28 2 2014 2014-02-28 10.1145/2559950 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2019-07-17T15:38:07.7889743 2013-02-26T10:39:43.6851048 Arnold Beckmann 0000-0001-7958-5790 1 Samuel R Buss 2
title Improved witnessing and local improvement principles for second-order bounded arithmetic
spellingShingle Improved witnessing and local improvement principles for second-order bounded arithmetic
Arnold Beckmann
title_short Improved witnessing and local improvement principles for second-order bounded arithmetic
title_full Improved witnessing and local improvement principles for second-order bounded arithmetic
title_fullStr Improved witnessing and local improvement principles for second-order bounded arithmetic
title_full_unstemmed Improved witnessing and local improvement principles for second-order bounded arithmetic
title_sort Improved witnessing and local improvement principles for second-order bounded arithmetic
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 ACM Transactions on Computational Logic
container_volume 15
container_issue 1
container_start_page 2:1
publishDate 2014
institution Swansea University
doi_str_mv 10.1145/2559950
document_store_str 0
active_str 0
description This paper concerns the second order systems U^1_2 and V^1_2 of bounded arithmetic, which have proof theoretic strengths corresponding to polynomial space and exponential time computation. We formulate improved witnessing theorems for these two theories by using S^1_2 as a base theory for proving the correctness of the polynomial space or exponential time witnessing functions. We develop the theory of nondeterministic polynomial space computation in U^1_2 . Kołodziejczyk, Nguyen, and Thapen have introduced local improvement properties to characterize the provably total NP functions of these second order theories. We show that the strengths of their local improvement principles over U^1_2 and V^1_2 depend primarily on the topology of the underlying graph, not the number of rounds in the local improvement games. The theory U^1_2 proves the local improvement principle for linear graphs even without restricting to logarithmically many rounds. The local improvement principle for grid graphs with only logarithmically rounds is complete for the provably total NP search problems of V^1_2 . Related results are obtained for local improvement principles with one improvement round, and for local improvement over rectangular grids.
published_date 2014-02-28T12:29:54Z
_version_ 1821408592468639744
score 11.123185

Similar Items