Cited By
View all- Duan LZhang XWang ZDuan F(2017)A Feasible Segment-by-Segment ALOHA Algorithm for RFID SystemsWireless Personal Communications: An International Journal10.1007/s11277-017-4316-y96:2(2633-2649)Online publication date: 1-Sep-2017
Quasipolynomial size proofs of the propositional pigeonhole principle
Author: 
Sam BussAuthors Info & Claims
Pages 77 - 84
Abstract
Cook and Reckhow proved in 1979 that the propositional pigeonhole principle has polynomial size extended Frege proofs. Buss proved in 1987 that it also has polynomial size Frege proofs; these Frege proofs used a completely different proof method based on counting. This paper shows that the original Cook and Reckhow extended Frege proofs can be formulated as quasipolynomial size Frege proofs. The key point is that st-connectivity can be used to define the Cook-Reckhow construction.
References
[1]
J. Aisenberg, M.L. Bonet, S. Buss, Quasipolynomial-size Frege proof of Frankl's theorem on the trace of finite sets, J. Symb. Log., forthcoming.
[2]
P. Beame, T. Pitassi, Propositional proof complexity: past, present and future, in: Current Trends in Theoretical Computer Science Entering the 21st Century, World Scientific, 2001, pp. 42-70.
[3]
A. Beckmann, S.R. Buss, Improved witnessing and local improvement principles for second-order bounded arithmetic, ACM Trans. Comput. Log., 15 (2014) 35.
[4]
M.L. Bonet, S.R. Buss, T. Pitassi, Are there hard examples for Frege systems?, in: Feasible Mathematics II, Birkhäuser, Boston, 1995, pp. 30-56.
[5]
S.R. Buss, Polynomial size proofs of the propositional pigeonhole principle, J. Symbolic Logic, 52 (1987) 916-927.
[6]
S.R. Buss, Propositional proof complexity: an introduction, in: Computational Logic, Springer-Verlag, Berlin, 1999, pp. 127-178.
[7]
S.R. Buss, Towards NP-P via proof complexity and proof search, Ann. Pure Appl. Logic, 163 (2012) 1163-1182.
[8]
S.A. Cook, R.A. Reckhow, The relative efficiency of propositional proof systems, J. Symbolic Logic, 44 (1979) 36-50.
[9]
P. Hrubeš, I. Tzameret, Short proofs for determinant identities, SIAM J. Comput. (2015).
[10]
G. Istrate, A. Crãciun, Proof complexity and the Kneser-Lovász theorem, in: Lecture Notes in Computer Science, vol. 8561, Springer Verlag, 2014, pp. 138-153.
[11]
L.A. Kołodziejczyk, P. Nguyen, N. Thapen, The provably total NP search problems of weak second-order bounded arithmetic, Ann. Pure Appl. Logic, 162 (2011) 419-446.
[12]
A. Maciel, T. Pitassi, A.R. Woods, A new proof of the weak pigeonhole principle, J. Comput. System Sci., 64 (2002) 843-872.
[13]
A. Nozaki, T. Arai, N.H. Arai, Polynomial-size Frege proofs of Bollobás' theorem on the trace of sets, Proc. Japan Acad. Ser. A Math. Sci., 84 (2008) 159-161.
[14]
C.H. Papadimitriou, On the complexity of the parity argument and other inefficient proofs of existence, J. Comput. System Sci., 48 (1994) 498-532.
[15]
J.B. Paris, A.J. Wilkie, A.R. Woods, Provability of the pigeonhole principle and the existence of infinitely many primes, J. Symbolic Logic, 53 (1988) 1235-1244.
[16]
N. Segerlind, The complexity of propositional proofs, Bull. Symbolic Logic, 13 (2007) 417-481.
- Quasipolynomial size proofs of the propositional pigeonhole principle
Recommendations
The NP Search Problems of Frege and Extended Frege Proofs
We study consistency search problems for Frege and extended Frege proofs—namely the NP search problems of finding syntactic errors in Frege and extended Frege proofs of contradictions. The input is a polynomial time function, or an oracle, describing a ...
Lower bounds for bounded depth Frege proofs via Pudlák-Buss games
We present a simple proof of the bounded-depth Frege proof lower bounds of Pitassi et al. [1993] and Krajíček et al. [1995] for the pigeonhole principle. Our method uses the interpretation of proofs as two player games given by Pudlák and Buss. Our ...
Characterizing Propositional Proofs as Noncommutative Formulas
Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional-calculus (i.e., Frege) proof is any proof starting from a set of axioms and deriving new Boolean formulas using a fixed set of sound derivation rules. ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Elsevier B.V.
Publisher
Elsevier Science Publishers Ltd.
United Kingdom
Publication History
Published: 20 April 2015
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 09 Dec 2024
Other Metrics
Citations
Cited By
View all- Duan LZhang XWang ZDuan F(2017)A Feasible Segment-by-Segment ALOHA Algorithm for RFID SystemsWireless Personal Communications: An International Journal10.1007/s11277-017-4316-y96:2(2633-2649)Online publication date: 1-Sep-2017
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in