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)
Separating DAG-Like and Tree-Like Proof Systems
Wroclaw, Poland
July 10-July 14
ISBN: 0-7695-2908-9
Phuong Nguyen, University of Toronto, Canada
We show that tree-like (Gentzen?s calculus) PK where all cut formulas have depth at most a constant d does not simulate cut-free PK. Generally, we exhibit a family of sequents that have polynomial size cut-free proofs but requires superpolynomial tree-like proofs even when the cut rule is allowed on a class of cut-formulas that satisfies some plausible hardness assumption. This gives (in some cases, conditional) negative answers to several questions from a recent work of Maciel and Pitassi (LICS 2006). Our technique is inspired by the technique from Maciel and Pitassi. While the sequents used in earlier work are derived from the Pigeonhole principle, here we generalize Statman?s sequents. This gives the desired separation, and at the same time provides stronger results in some cases.
Citation:
Phuong Nguyen, "Separating DAG-Like and Tree-Like Proof Systems," lics, pp.235-244, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.