No Cover Image

Journal article 604 views

Improved witnessing and local improvement principles for second-order bounded arithmetic / Arnold Beckmann; Samuel R Buss

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

Swansea University Author: Arnold, Beckmann

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
Tags: Add Tag
No Tags, Be the first to tag this record!
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ł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.
Issue: 1
Start Page: 2:1
End Page: 2:35