Our main result shows that a shortest proof size of tree-like resolution for the pigeonhole principle is superpolynomially larger than that of DAG-like resolution. In the proof of a lower bound, we exploit a relationship between tree-like resolution and backtracking, which has long been recognized in this field but not been used before to give explicit results.
CITATION STYLE
Iwama, K., & Miyazaki, S. (1999). Tree-like resolution is superpolynomially slower than dag-like resolution for the pigeonhole principle. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1741, pp. 133–142). Springer Verlag. https://doi.org/10.1007/3-540-46632-0_14
Mendeley helps you to discover research relevant for your work.