On Small-depth Frege Proofs for Tseitin for Grids
- 17 November 2020
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 68 (1), 1-31
- https://doi.org/10.1145/3425606
Abstract
We prove that a small-depth Frege refutation of the Tseitin contradiction on the grid requires subexponential size. We conclude that polynomial size Frege refutations of the Tseitin contradiction must use formulas of almost logarithmic depth.Keywords
This publication has 16 references indexed in Scilit:
- Hard examples for the bounded depth Frege proof systemcomputational complexity, 2002
- Short proofs are narrow—resolution made simpleJournal of the ACM, 2001
- Simplified Lower Bounds for Propositional ProofsNotre Dame Journal of Formal Logic, 1996
- An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principleRandom Structures & Algorithms, 1995
- The complexity of the Pigeonhole PrincipleCombinatorica, 1994
- Exponential lower bounds for the pigeonhole principlecomputational complexity, 1993
- Approximation and Small-Depth Frege ProofsSIAM Journal on Computing, 1992
- Polynomial size proofs of the propositional pigeonhole principleThe Journal of Symbolic Logic, 1987
- The intractability of resolutionTheoretical Computer Science, 1985
- Parity, circuits, and the polynomial-time hierarchyTheory of Computing Systems, 1984