loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)
Examining The Fragments of G
Wroclaw, Poland
July 10-July 14
ISBN: 0-7695-2908-9
Steven James Perron, University of Toronto, Canada
When restricted to proving \Sigma _i^q i formulas, the quantified propositional proof system G_i^* is closely related to the \Sigma_i^b theorems of Buss's theory S_2^i . Namely, G_i^* has polynomialsize proofs of the translations of theorems of S_2^i , and S_2^i proves that G_i^* is sound. However, little is known about G_i^* when proving more complex formulas. In this paper, we prove a witnessing theorem for G_1^* similar in style to the KPT witnessing theorem for T_2^i. This witnessing theorem is then used to show that S_2^i proves G_1^* is sound with respect to prenex \Sigma_i+1^q formulas. Note that unless the polynomial hierarchy collapses S_2^i is the weakest theory in the S_2 hierarchy for which this is true. The witnessing theorem is also used to show that G_1^* is p-equivalent to a quantified version of extended-Frege. This is followed by a proof that G_i p-simulates G_i+1^*. We finish by proving that S_2 can be axiomatized by S_2^1 plus axioms stating that the cut-free version of G* is sound. All together this shows that the connection between G_i^* and S_2^i does not extend to more complex formulas.
Citation:
Steven James Perron, "Examining The Fragments of G," lics, pp.225-234, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.