Switch to: Citations

References in:

The limits of tractability in Resolution-based propositional proof systems

Stefan Dantchev & Barnaby Martin

Annals of Pure and Applied Logic 163 (6):656-668 (2012)

Add references

You must login to add references.

Lower Bounds to the size of constant-depth propositional proofs.Jan Krajíček - 1994 - Journal of Symbolic Logic 59 (1):73-86.details LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and $\bigwedge, \bigvee$. Then for every d ≥ 0 and n ≥ 2, there is a set Td n of depth d sequents of total size O which are refutable in LK by depth d + 1 proof of size exp) but such that every depth d refutation must have the size at least exp). The sets Td n express a weaker form of the pigeonhole (...) principle. (shrink) Download Export citation Bookmark 21 citations
The limits of tractability in Resolution-based propositional proof systems.Stefan Dantchev & Barnaby Martin - 2012 - Annals of Pure and Applied Logic 163 (6):656-668.details Download Export citation Bookmark 1 citation
Separation results for the size of constant-depth propositional proofs.Arnold Beckmann & Samuel R. Buss - 2005 - Annals of Pure and Applied Logic 136 (1-2):30-55.details This paper proves exponential separations between depth d-LK and depth -LK for every utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d-LK and depth -LK for . We investigate the relationship between the sequence-size, tree-size and height of depth d-LK-derivations for , and describe transformations between them. We define a general method to lift principles requiring exponential tree-size -LK-refutations for to principles requiring exponential sequence-size d-LK-refutations, which will be described for the Ramsey principle (...) Download Export citation Bookmark 4 citations

1