Sciweavers

LICS
2007
IEEE

Separating DAG-Like and Tree-Like Proof Systems

14 years 5 months ago
Separating DAG-Like and Tree-Like Proof Systems
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.
Phuong Nguyen
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where LICS
Authors Phuong Nguyen
Comments (0)