Quantified Propositional Logspace Reasoning
| dc.creator | Perron, Steven | |
| dc.date | 2008-01-27 | |
| dc.date.accessioned | 2026-07-07T08:56:43Z | |
| dc.date.available | 2026-07-07T08:56:43Z | |
| dc.description | In this paper, we develop a quantified propositional proof systems that corresponds to logarithmic-space reasoning. We begin by defining a class SigmaCNF(2) of quantified formulas that can be evaluated in log space. Then our new proof system GL^* is defined as G_1^* with cuts restricted to SigmaCNF(2) formulas and no cut formula that is not quantifier free contains a free variable that does not appear in the final formula. To show that GL^* is strong enough to capture log space reasoning, we translate theorems of VL into a family of tautologies that have polynomial-size GL^* proofs. VL is a theory of bounded arithmetic that is known to correspond to logarithmic-space reasoning. To do the translation, we find an appropriate axiomatization of VL, and put VL proofs into a new normal form. To show that GL^* is not too strong, we prove the soundness of GL^* in such a way that it can be formalized in VL. This is done by giving a logarithmic-space algorithm that witnesses GL^* proofs. | |
| dc.description | 28 pages | |
| dc.identifier | https://arxiv.org/abs/0801.4105 | |
| dc.identifier | http://arxiv.org/abs/0801.4105 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/146713 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | Computational Complexity | |
| dc.title | Quantified Propositional Logspace Reasoning | |
| dc.type | text |