Sciweavers

LICS
2007
IEEE
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 t...
Phuong Nguyen