Sciweavers

CSL
2004
Springer

A Third-Order Bounded Arithmetic Theory for PSPACE

14 years 5 months ago
A Third-Order Bounded Arithmetic Theory for PSPACE
We present a novel third-order theory W1 1 of bounded arithmetic suitable for reasoning about PSPACE functions. This theory has the advantages of avoiding the smash function symbol and is otherwise much simpler than previous PSPACE theories. As an example we outline a proof in W1 1 that from any configuration in the game of Hex, at least one player has a winning strategy. We then exhibit a translation of theorems of W1 1 into families of propositional tautologies with polynomial-size proofs in BPLK (a recent propositional proof system for PSPACE and an alternative to G). This translation is clearer and more natural in several respects than the analogous ones for previous PSPACE theories.
Alan Skelley
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CSL
Authors Alan Skelley
Comments (0)