Computer Science – Logic in Computer Science
Scientific paper
2008-01-27
Computer Science
Logic in Computer Science
28 pages
Scientific paper
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.
No associations
LandOfFree
Quantified Propositional Logspace Reasoning does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Quantified Propositional Logspace Reasoning, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Quantified Propositional Logspace Reasoning will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-313545