@article{Haken:TCS:1985,
    Abstract = {We prove that, for infinitely many disjunctive normal form propositional calculus tautologies ξ, the length of the shortest resolution proof of ξ cannot be bounded by any polynomial of the length of ξ. The tautologies we use were introduced by Cook and Reckhow (1979) and encode the pigeonhole principle. Extended resolution can furnish polynomial length proofs of these formulas.},
    Author = {Haken, Armin},
    File = {The intractability of resolution - 1-s2.0-0304397585901446-main - a - a - f.pdf},
    ISSN = {0304-3975},
    Journal = {Theoretical Computer Science},
    Note = {Third Conference on Foundations of Software Technology and Theoretical Computer Science},
    Pages = {297--308},
    Title = {The intractability of resolution},
    URL = {http://www.sciencedirect.com/science/article/pii/0304397585901446},
    Volume = {39},
    Year = {1985},
    bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/0304397585901446},
    bdsk-url-2 = {https://doi.org/10.1016/0304-3975(85)90144-6},
    date-added = {2019-10-14 17:34:34 +0200},
    date-modified = {2019-10-15 14:50:55 +0200},
    doi = {10.1016/0304-3975(85)90144-6}
}

@article{Haken:TCS:1985, Abstract = {We prove that, for infinitely many disjunctive normal form propositional calculus tautologies ξ, the length of the shortest resolution proof of ξ cannot be bounded by any polynomial of the length of ξ. The tautologies we use were introduced by Cook and Reckhow (1979) and encode the pigeonhole principle. Extended resolution can furnish polynomial length proofs of these formulas.}, Author = {Haken, Armin}, File = {The intractability of resolution - 1-s2.0-0304397585901446-main - a - a - f.pdf}, ISSN = {0304-3975}, Journal = {Theoretical Computer Science}, Note = {Third Conference on Foundations of Software Technology and Theoretical Computer Science}, Pages = {297--308}, Title = {The intractability of resolution}, URL = {http://www.sciencedirect.com/science/article/pii/0304397585901446}, Volume = {39}, Year = {1985}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/0304397585901446}, bdsk-url-2 = {https://doi.org/10.1016/0304-3975(85)90144-6}, date-added = {2019-10-14 17:34:34 +0200}, date-modified = {2019-10-15 14:50:55 +0200}, doi = {10.1016/0304-3975(85)90144-6} }