Lower bounds to the size of constant-depth propositional proofs
- 12 March 1994
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 59 (1) , 73-86
- https://doi.org/10.2307/2275250
Abstract
LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and ∧,∨ (both of bounded arity). Then for every d ≥ 0 and n ≥ 2, there is a set of depth d sequents of total size O(n3+d) which are refutable in LK by depth d + 1 proof of size exp(O(log2n)) but such that every depth d refutation must have the size at least exp(nΩ(1)). The sets express a weaker form of the pigeonhole principle.Keywords
This publication has 12 references indexed in Scilit:
- Exponential lower bounds for the pigeonhole principlecomputational complexity, 1993
- Fragments of bounded arithmetic and bounded query classesTransactions of the American Mathematical Society, 1993
- Approximation and Small-Depth Frege ProofsSIAM Journal on Computing, 1992
- Parity and the Pigeonhole PrinciplePublished by Springer Nature ,1990
- Axiomatizations and conservation results for fragments of bounded arithmeticPublished by American Mathematical Society (AMS) ,1990
- Resolution proofs of generalized pigeonhole principlesTheoretical Computer Science, 1988
- The intractability of resolutionTheoretical Computer Science, 1985
- Counting problems in bounded arithmeticLecture Notes in Mathematics, 1985
- Bounds for proof-search and speed-up in the predicate calculusAnnals of Mathematical Logic, 1978
- Normal derivability in classical logicLecture Notes in Mathematics, 1968