No Cover Image

Book chapter 1036 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
Tags: Add Tag
No Tags, Be the first to tag this record!
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)$.
College: Faculty of Science and Engineering
Start Page: 65
End Page: 134

Similar Items