Abstract
A pseudorandom generator $G_n:\{0,1\}^n\to \{0,1\}^m$ is hard for a propositional proof system $P$ if (roughly speaking) $P$ cannot efficiently prove the statement $G_n(x_1,\ldots,x_n)\neq b$ for any string $b\in\{0,1\}^m$. We present a function ($m\geq 2^{n^{\Omega(1)}}$) generator which is hard for $\mathrm{Res}(\epsilon\log n)$; here $\mathrm{Res}(k)$ is the propositional proof system that extends Resolution by allowing $k$-DNFs instead of clauses.
As a direct consequence of this result, we show that whenever $t\geq n^2$, every $\mathrm{Res}(\epsilon\log t)$ proof of the principle $\neg \mathrm{Circuit}_t(f_n)$ (asserting that the circuit size of a Boolean function $f_n$ in $n$ variables is greater than $t$) must have size $\exp(t^{\Omega(1)})$. In particular, $\mathrm{Res}(\log \log N)$ ($N\sim 2^n$ is the overall number of propositional variables) does not possess efficient proofs of ${\bf NP}\not\subseteq {\bf P}/\mathrm{poly}$. Similar results hold also for the system PCR (the natural common extension of Polynomial Calculus and Resolution) when the characteristic of the ground field is different from 2.
As a byproduct, we also improve on the small restriction switching lemma due to Segerlind, Buss and Impagliazzo by removing a square root from the final bound. This in particular implies that the (moderately) weak pigeonhole principle $\mathrm{PHP}^{2n}_n$ is hard for $\mathrm{Res}(\epsilon\log n/\log\log n)$.
-
[ABE]
A. Atserias, M. L. Bonet, and J. L. Esteban, "Lower bounds for the weak pigeonhole principle and random formulas beyond Resolution," Inform. and Comput., vol. 176, iss. 2, pp. 136-152, 2002.
@article{ABE, mrkey = {1923576},
author = {Atserias, Albert and Bonet, Maria Luisa and Esteban, Juan Luis},
title = {Lower bounds for the weak pigeonhole principle and random formulas beyond {R}esolution},
journal = {Inform. and Comput.},
fjournal = {Information and Computation},
volume = {176},
year = {2002},
number = {2},
pages = {136--152},
issn = {0890-5401},
mrclass = {03F20 (03F30 60C05 68Q15)},
mrnumber = {1923576},
mrreviewer = {Jan Kraj{\'ı}{\v{c}}ek},
doi = {10.1006/inco.2002.3114},
zblnumber = {1012.03058},
} -
[spaceres]
M. Alekhnovich, E. Ben-Sasson, A. A. Razborov, and A. Wigderson, "Space complexity in propositional calculus," SIAM J. Comput., vol. 31, iss. 4, pp. 1184-1211, 2002.
@article{spaceres, mrkey = {1919962},
author = {Alekhnovich, Michael and Ben-Sasson, Eli and Razborov, Alexander A. and Wigderson, Avi},
title = {Space complexity in propositional calculus},
journal = {SIAM J. Comput.},
fjournal = {SIAM Journal on Computing},
volume = {31},
year = {2002},
number = {4},
pages = {1184--1211},
issn = {0097-5397},
mrclass = {03F20 (68Q15 68Q17 68Q25)},
mrnumber = {1919962},
mrreviewer = {G. E. Mints},
doi = {10.1137/S0097539700366735},
zblnumber = {1004.03047},
} -
[generate]
M. Alekhnovich, E. Ben-Sasson, A. A. Razborov, and A. Wigderson, "Pseudorandom generators in propositional proof complexity," SIAM J. Comput., vol. 34, iss. 1, pp. 67-88, 2004.
@article{generate, mrkey = {2114305},
author = {Alekhnovich, Michael and Ben-Sasson, Eli and Razborov, Alexander A. and Wigderson, Avi},
title = {Pseudorandom generators in propositional proof complexity},
journal = {SIAM J. Comput.},
fjournal = {SIAM Journal on Computing},
volume = {34},
year = {2004},
number = {1},
pages = {67--88},
issn = {0097-5397},
mrclass = {03F20 (03D15)},
mrnumber = {2114305},
mrreviewer = {Christopher J. Pollett},
doi = {10.1137/S0097539701389944},
zblnumber = {1096.03070},
} -
[misha:eng] M. V. Alekhnovich and A. A. Razborov, "Lower bounds for polynomial calculus: the nonbinomial ideal case," Tr. Mat. Inst. Steklova, vol. 242, iss. Mat. Logika i Algebra, pp. 23-43, 2003.
@article{misha:eng, mrkey = {2054483},
author = {Alekhnovich, M. V. and Razborov, A. A.},
title = {Lower bounds for polynomial calculus: the nonbinomial ideal case},
journal = {Tr. Mat. Inst. Steklova},
fjournal = {Trudy Matematicheskogo Instituta Imeni V. A. Steklova. Rossiĭskaya Akademiya Nauk},
volume = {242},
year = {2003},
number = {Mat. Logika i Algebra},
pages = {23--43},
issn = {0371-9685},
mrclass = {03F20 (06E30 68Q17)},
mrnumber = {2054483},
mrreviewer = {M. I. Dekhtyar},
zblnumber = {1079.03047},
} -
[AlS]
N. Alon and J. H. Spencer, The probabilistic method, Third ed., Hoboken, NJ: John Wiley & Sons, 2008.
@book{AlS, mrkey = {2437651},
author = {Alon, Noga and Spencer, Joel H.},
title = {The probabilistic method},
series = {Wiley-Intersci. Ser. Discr. Math. Optim.},
edition = {Third},
publisher = {John Wiley \& Sons},
address = {Hoboken, NJ},
year = {2008},
pages = {xviii+352},
isbn = {978-0-470-17020-5},
mrclass = {60-02 (05C80 60C05 60F99 60G42)},
mrnumber = {2437651},
doi = {10.1002/9780470277331},
zblnumber = {1148.05001},
} -
[BBC*] R. Beals, H. Buhrman, R. Cleve, M. Mosca, and R. de Wolf, "Quantum lower bounds by polynomials," J. ACM, vol. 48, pp. 778-797, 2001.
@article{BBC*,
author = {Beals, R. and Buhrman, H. and Cleve, R. and Mosca, M. and de~Wolf, R.},
title = {Quantum lower bounds by polynomials},
journal = {J. ACM},
volume = {48},
year = {2001},
pages = {778--797},
zblnumber = {1127.68404},
} -
[BGI*]
S. Buss, D. Grigoriev, R. Impagliazzo, and T. Pitassi, "Linear gaps between degrees for the polynomial calculus modulo distinct primes," J. Comput. System Sci., vol. 62, iss. 2, pp. 267-289, 2001.
@article{BGI*, mrkey = {1820593},
author = {Buss, Sam and Grigoriev, Dima and Impagliazzo, Russell and Pitassi, Toniann},
title = {Linear gaps between degrees for the polynomial calculus modulo distinct primes},
journal = {J. Comput. System Sci.},
fjournal = {Journal of Computer and System Sciences},
volume = {62},
year = {2001},
number = {2},
pages = {267--289},
issn = {0022-0000},
coden = {JCSSBM},
mrclass = {03F20 (68Q17 68Q25)},
mrnumber = {1820593},
mrreviewer = {Søren M. Riis},
doi = {10.1006/jcss.2000.1726},
} -
[BeI]
E. Ben-Sasson and R. Impagliazzo, "Random CNF’s are hard for the polynomial calculus," Comput. Complexity, vol. 19, iss. 4, pp. 501-519, 2010.
@article{BeI, mrkey = {2746277},
author = {Ben-Sasson, Eli and Impagliazzo, Russell},
title = {Random {CNF}'s are hard for the polynomial calculus},
journal = {Comput. Complexity},
fjournal = {Computational Complexity},
volume = {19},
year = {2010},
number = {4},
pages = {501--519},
issn = {1016-3328},
coden = {CPTCEU},
mrclass = {03F20 (03B05 68Q17)},
mrnumber = {2746277},
mrreviewer = {Jochen Messner},
doi = {10.1007/s00037-010-0293-1},
zblnumber = {1216.03064},
} -
[BeP1]
P. Beame and T. Pitassi, "Simplified and improved resolution lower bounds," in 37th Annual Symposium on Foundations of Computer Science, Los Alamitos, CA: IEEE Comput. Soc. Press, 1996, pp. 274-282.
@incollection{BeP1, mrkey = {1450625},
author = {Beame, Paul and Pitassi, Toniann},
title = {Simplified and improved resolution lower bounds},
booktitle = {37th {A}nnual {S}ymposium on {F}oundations of {C}omputer {S}cience},
venue = {{B}urlington, {VT},
1996},
pages = {274--282},
publisher = {IEEE Comput. Soc. Press},
address = {Los Alamitos, CA},
year = {1996},
mrclass = {68Q25 (03B35 03D15 68T15)},
mrnumber = {1450625},
doi = {10.1109/SFCS.1996.548486},
} -
[BeP2] P. Beame and T. Pitassi, "Propositional proof complexity: past, present, and future," in Current Trends in Theoretical Computer Science, River Edge, NJ: World Sci. Publ., 2001, pp. 42-70.
@incollection{BeP2, mrkey = {1886033},
author = {Beame, Paul and Pitassi, Toniann},
title = {Propositional proof complexity: past, present, and future},
booktitle = {Current Trends in Theoretical Computer Science},
pages = {42--70},
publisher = {World Sci. Publ.},
address = {River Edge, NJ},
year = {2001},
mrclass = {03F20 (68Q15)},
mrnumber = {1886033},
zblnumber = {1049.03040},
} -
[BPR]
M. Bonet, T. Pitassi, and R. Raz, "Lower bounds for cutting planes proofs with small coefficients," J. Symbolic Logic, vol. 62, iss. 3, pp. 708-728, 1997.
@article{BPR, mrkey = {1472120},
author = {Bonet, Maria and Pitassi, Toniann and Raz, Ran},
title = {Lower bounds for cutting planes proofs with small coefficients},
journal = {J. Symbolic Logic},
fjournal = {The Journal of Symbolic Logic},
volume = {62},
year = {1997},
number = {3},
pages = {708--728},
issn = {0022-4812},
coden = {JSYLA6},
mrclass = {03D15 (03F20 68Q15)},
mrnumber = {1472120},
mrreviewer = {M. Tetruashvili},
doi = {10.2307/2275569},
zblnumber = {0889.03050},
} -
[BPR1]
M. L. Bonet, T. Pitassi, and R. Raz, "On interpolation and automatization for Frege systems," SIAM J. Comput., vol. 29, iss. 6, pp. 1939-1967, 2000.
@article{BPR1, mrkey = {1756400},
author = {Bonet, Maria Luisa and Pitassi, Toniann and Raz, Ran},
title = {On interpolation and automatization for {F}rege systems},
journal = {SIAM J. Comput.},
fjournal = {SIAM Journal on Computing},
volume = {29},
year = {2000},
number = {6},
pages = {1939--1967},
issn = {0097-5397},
mrclass = {03F20 (03D15 68Q15 68Q17)},
mrnumber = {1756400},
mrreviewer = {Piotr Wojtylak},
doi = {10.1137/S0097539798353230},
zblnumber = {0959.03044},
} -
[BuT]
S. R. Buss and G. Turán, "Resolution proofs of generalized pigeonhole principles," Theoret. Comput. Sci., vol. 62, iss. 3, pp. 311-317, 1988.
@article{BuT, mrkey = {0980936},
author = {Buss, Samuel R. and Tur{á}n, Gy{ö}rgy},
title = {Resolution proofs of generalized pigeonhole principles},
journal = {Theoret. Comput. Sci.},
fjournal = {Theoretical Computer Science},
volume = {62},
year = {1988},
number = {3},
pages = {311--317},
issn = {0304-3975},
coden = {TCSDI},
mrclass = {68T15 (03B35 03D15 68Q25)},
mrnumber = {0980936},
mrreviewer = {G. E. Peterson},
doi = {10.1016/0304-3975(88)90072-2},
zblnumber = {1007.03052},
} -
[CEI]
M. Clegg, J. Edmonds, and R. Impagliazzo, "Using the Groebner basis algorithm to find proofs of unsatisfiability," in Proceedings of the Twenty-eighth Annual ACM Symposium on the Theory of Computing, New York, 1996, pp. 174-183.
@inproceedings{CEI, mrkey = {1427512},
author = {Clegg, Matthew and Edmonds, Jeffery and Impagliazzo, Russell},
title = {Using the {G}roebner basis algorithm to find proofs of unsatisfiability},
booktitle = {Proceedings of the {T}wenty-eighth {A}nnual {ACM} {S}ymposium on the {T}heory of {C}omputing},
venue = {{P}hiladelphia, {PA},
1996},
pages = {174--183},
publisher = {ACM},
address = {New York},
year = {1996},
mrclass = {68T15 (68Q35 68Q40)},
mrnumber = {1427512},
doi = {10.1145/237814.237860},
zblnumber = {0938.68825},
} -
[CRV*]
M. Capalbo, O. Reingold, S. Vadhan, and A. Wigderson, "Randomness conductors and constant-degree lossless expanders," in Proceedings of the Thirty-Fourth Annual ACM Symposium on Theory of Computing, New York, 2002, pp. 659-668.
@inproceedings{CRV*, mrkey = {2121193},
author = {Capalbo, Michael and Reingold, Omer and Vadhan, Salil and Wigderson, Avi},
title = {Randomness conductors and constant-degree lossless expanders},
booktitle = {Proceedings of the {T}hirty-{F}ourth {A}nnual {ACM} {S}ymposium on {T}heory of {C}omputing},
pages = {659--668},
publisher = {ACM},
address = {New York},
year = {2002},
mrclass = {68R10 (68W20)},
mrnumber = {2121193},
doi = {10.1145/509907.510003},
zblnumber = {1192.68475},
} -
[GGM]
O. Goldreich, S. Goldwasser, and S. Micali, "How to construct random functions," J. Assoc. Comput. Mach., vol. 33, iss. 4, pp. 792-807, 1986.
@article{GGM, mrkey = {0860526},
author = {Goldreich, Oded and Goldwasser, Shafi and Micali, Silvio},
title = {How to construct random functions},
journal = {J. Assoc. Comput. Mach.},
fjournal = {Journal of the Association for Computing Machinery},
volume = {33},
year = {1986},
number = {4},
pages = {792--807},
issn = {0004-5411},
coden = {JACOAH},
mrclass = {68Q30 (68Q25)},
mrnumber = {0860526},
mrreviewer = {P. G{á}cs},
doi = {10.1145/6490.6503},
zblnumber = {0596.65002},
} -
[Gol]
O. Goldreich, "Candidate one-way functions based on expander graphs," in Studies in Complexity and Cryptography, New York: Springer-Verlag, 2011, vol. 6650, pp. 76-87.
@incollection{Gol, mrkey = {2844254},
author = {Goldreich, Oded},
title = {Candidate one-way functions based on expander graphs},
booktitle = {Studies in Complexity and Cryptography},
series = {Lecture Notes in Comput. Sci.},
volume = {6650},
pages = {76--87},
publisher = {Springer-Verlag},
year = {2011},
mrclass = {94A60 (05C75 05C90)},
mrnumber = {2844254},
mrreviewer = {D. J. Guan},
doi = {10.1007/978-3-642-22670-0_10},
address = {New York},
zblnumber = {05940578},
} -
[IKW]
R. Impagliazzo, V. Kabanets, and A. Wigderson, "In search of an easy witness: exponential time vs. probabilistic polynomial time," J. Comput. System Sci., vol. 65, iss. 4, pp. 672-694, 2002.
@article{IKW, mrkey = {1964649},
author = {Impagliazzo, Russell and Kabanets, Valentine and Wigderson, Avi},
title = {In search of an easy witness: exponential time vs. probabilistic polynomial time},
journal = {J. Comput. System Sci.},
fjournal = {Journal of Computer and System Sciences},
volume = {65},
year = {2002},
number = {4},
pages = {672--694},
issn = {0022-0000},
coden = {JCSSBM},
mrclass = {68Q15 (94C10)},
mrnumber = {1964649},
doi = {10.1016/S0022-0000(02)00024-7},
zblnumber = {1059.68047},
} -
[Jan]
S. Janson, "Poisson approximation for large deviations," Random Structures Algorithms, vol. 1, iss. 2, pp. 221-229, 1990.
@article{Jan, mrkey = {1138428},
author = {Janson, Svante},
title = {Poisson approximation for large deviations},
journal = {Random Structures Algorithms},
fjournal = {Random Structures \& Algorithms},
volume = {1},
year = {1990},
number = {2},
pages = {221--229},
issn = {1042-9832},
mrclass = {60F10 (05C80 60C05)},
mrnumber = {1138428},
mrreviewer = {Andrew D. Barbour},
doi = {10.1002/rsa.3240010209},
zblnumber = {0747.05079},
} -
[KrP]
J. Kraj’ivcek and P. Pudlák, "Some consequences of cryptographical conjectures for ${ S}^1_2$ and ${ EF}$," Inform. and Comput., vol. 140, iss. 1, pp. 82-94, 1998.
@article{KrP, mrkey = {1492845},
author = {Kraj{\'ı}{\v{c}}ek, Jan and Pudl{á}k, Pavel},
title = {Some consequences of cryptographical conjectures for {${\rm S}\sp 1\sb 2$} and {${\rm EF}$}},
journal = {Inform. and Comput.},
fjournal = {Information and Computation},
volume = {140},
year = {1998},
number = {1},
pages = {82--94},
issn = {0890-5401},
mrclass = {03F30 (03F20 68P25 68Q15 94A60)},
mrnumber = {1492845},
mrreviewer = {Roman Murawski},
doi = {10.1006/inco.1997.2674},
zblnumber = {0892.68029},
} -
[Kraj2]
J. Kraj’ivcek, Bounded Arithmetic, Propositional Logic, and Complexity Theory, Cambridge: Cambridge Univ. Press, 1995, vol. 60.
@book{Kraj2, mrkey = {1366417},
author = {Kraj{\'ı}{\v{c}}ek, Jan},
title = {Bounded Arithmetic, Propositional Logic, and Complexity Theory},
series = {Encyclopedia Math. Appl.},
volume = {60},
publisher = {Cambridge Univ. Press},
address = {Cambridge},
year = {1995},
pages = {xiv+343},
isbn = {0-521-45205-8},
mrclass = {03-02 (03D15 03Fxx 68Q15)},
mrnumber = {1366417},
mrreviewer = {Constantine Dimitracopoulos},
doi = {10.1017/CBO9780511529948},
zblnumber = {0835.03025},
} -
[Kraj3]
J. Kraj’ivcek, "Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic," J. Symbolic Logic, vol. 62, iss. 2, pp. 457-486, 1997.
@article{Kraj3, mrkey = {1464108},
author = {Kraj{\'ı}{\v{c}}ek, Jan},
title = {Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic},
journal = {J. Symbolic Logic},
fjournal = {The Journal of Symbolic Logic},
volume = {62},
year = {1997},
number = {2},
pages = {457--486},
issn = {0022-4812},
coden = {JSYLA6},
mrclass = {03F20 (03B05 03F30 68Q25)},
mrnumber = {1464108},
mrreviewer = {G. E. Mints},
doi = {10.2307/2275541},
zblnumber = {0891.03029},
} -
[Kraj7]
J. Kraj’ivcek, "Lower bounds for a proof system with an exponential speed-up over constant-depth Frege systems and over polynomial calculus," in Mathematical Foundations of Computer Science 1997, New York: Springer-Verlag, 1997, vol. 1295, pp. 85-90.
@incollection{Kraj7, mrkey = {1640210},
author = {Kraj{\'ı}{\v{c}}ek, Jan},
title = {Lower bounds for a proof system with an exponential speed-up over constant-depth {F}rege systems and over polynomial calculus},
booktitle = {Mathematical Foundations of Computer Science 1997},
venue = {{B}ratislava},
series = {Lecture Notes in Comput. Sci.},
volume = {1295},
pages = {85--90},
publisher = {Springer-Verlag},
year = {1997},
mrclass = {03F20},
mrnumber = {1640210},
doi = {10.1007/BFb0029951},
address = {New York},
zblnumber = {0935.03068},
} -
[Kraj9]
J. Kraj’ivcek, "On the weak pigeonhole principle," Fund. Math., vol. 170, iss. 1-2, pp. 123-140, 2001.
@article{Kraj9, mrkey = {1881373},
author = {Kraj{\'ı}{\v{c}}ek, Jan},
title = {On the weak pigeonhole principle},
journal = {Fund. Math.},
fjournal = {Fundamenta Mathematicae},
volume = {170},
year = {2001},
number = {1-2},
pages = {123--140},
issn = {0016-2736},
mrclass = {03F20 (03F30 68P25 68Q17 94A60)},
mrnumber = {1881373},
doi = {10.4064/fm170-1-8},
zblnumber = {0987.03051},
} -
[Kraj11]
J. Kraj’ivcek, "Tautologies from pseudo-random generators," Bull. Symbolic Logic, vol. 7, iss. 2, pp. 197-212, 2001.
@article{Kraj11, mrkey = {1839545},
author = {Kraj{\'ı}{\v{c}}ek, Jan},
title = {Tautologies from pseudo-random generators},
journal = {Bull. Symbolic Logic},
fjournal = {The Bulletin of Symbolic Logic},
volume = {7},
year = {2001},
number = {2},
pages = {197--212},
issn = {1079-8986},
mrclass = {03F20 (03F30)},
mrnumber = {1839545},
mrreviewer = {Søren M. Riis},
doi = {10.2307/2687774},
zblnumber = {0983.03046},
} -
[Kraj10]
J. Kraj’ivcek, "Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds," J. Symbolic Logic, vol. 69, iss. 1, pp. 265-286, 2004.
@article{Kraj10, mrkey = {2039361},
author = {Kraj{\'ı}{\v{c}}ek, Jan},
title = {Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds},
journal = {J. Symbolic Logic},
fjournal = {The Journal of Symbolic Logic},
volume = {69},
year = {2004},
number = {1},
pages = {265--286},
issn = {0022-4812},
coden = {JSYLA6},
mrclass = {03F20 (68Q17)},
mrnumber = {2039361},
mrreviewer = {Christopher J. Pollett},
doi = {10.2178/jsl/1080938841},
zblnumber = {1068.03048},
} -
[Nisa]
N. Nisan, "CREW PRAMs and decision trees," SIAM J. Comput., vol. 20, iss. 6, pp. 999-1007, 1991.
@article{Nisa, mrkey = {1135744},
author = {Nisan, Noam},
title = {C{REW} {PRAM}s and decision trees},
journal = {SIAM J. Comput.},
fjournal = {SIAM Journal on Computing},
volume = {20},
year = {1991},
number = {6},
pages = {999--1007},
issn = {0097-5397},
coden = {SMJCAT},
mrclass = {68Q25 (68Q10)},
mrnumber = {1135744},
doi = {10.1137/0220062},
zblnumber = {0737.68028},
} -
[NiW]
N. Nisan and A. Wigderson, "Hardness vs. randomness," J. Comput. System Sci., vol. 49, iss. 2, pp. 149-167, 1994.
@article{NiW, mrkey = {1293639},
author = {Nisan, Noam and Wigderson, Avi},
title = {Hardness vs. randomness},
journal = {J. Comput. System Sci.},
fjournal = {Journal of Computer and System Sciences},
volume = {49},
year = {1994},
number = {2},
pages = {149--167},
issn = {0022-0000},
coden = {JCSSBM},
mrclass = {68Q15 (65C10)},
mrnumber = {1293639},
mrreviewer = {Wen Qi Huang},
doi = {10.1016/S0022-0000(05)80043-1},
zblnumber = {0821.68057},
} -
[Pin] M. Pinsker, "On the complexity of a concentrator," in 7th Annual Teletraffic Conference, Stockholm: , 1973, p. 318/1-318/4.
@incollection{Pin,
author = {Pinsker, M.},
title = {On the complexity of a concentrator},
booktitle = {{\rm 7}th Annual Teletraffic Conference},
pages = {318/1--318/4},
address = {Stockholm},
year = {1973},
} -
[Pud4]
P. Pudlák, "Lower bounds for resolution and cutting plane proofs and monotone computations," J. Symbolic Logic, vol. 62, iss. 3, pp. 981-998, 1997.
@article{Pud4, mrkey = {1472134},
author = {Pudl{á}k, Pavel},
title = {Lower bounds for resolution and cutting plane proofs and monotone computations},
journal = {J. Symbolic Logic},
fjournal = {The Journal of Symbolic Logic},
volume = {62},
year = {1997},
number = {3},
pages = {981--998},
issn = {0022-4812},
coden = {JSYLA6},
mrclass = {03F20 (68Q15)},
mrnumber = {1472134},
mrreviewer = {M. Tetruashvili},
doi = {10.2307/2275583},
zblnumber = {0945.03086},
} -
[Pud5]
P. Pudlák, "The lengths of proofs," in Handbook of Proof Theory, Amsterdam: North-Holland, 1998, pp. 547-637.
@incollection{Pud5, mrkey = {1640332},
author = {Pudl{á}k, Pavel},
title = {The lengths of proofs},
booktitle = {Handbook of Proof Theory},
series = {Stud. Logic Found. Math.},
volumew = {137},
pages = {547--637},
publisher = {North-Holland},
address = {Amsterdam},
year = {1998},
mrclass = {03F20 (03B35 68T15)},
mrnumber = {1640332},
mrreviewer = {M. I. Dekhtyar},
doi = {10.1016/S0049-237X(98)80023-2},
zblnumber = {0920.03056},
} -
[Raz3]
R. Raz, "Resolution lower bounds for the weak pigeonhole principle," J. ACM, vol. 51, iss. 2, pp. 115-138, 2004.
@article{Raz3, mrkey = {2145651},
author = {Raz, Ran},
title = {Resolution lower bounds for the weak pigeonhole principle},
journal = {J. ACM},
fjournal = {Journal of the ACM},
volume = {51},
year = {2004},
number = {2},
pages = {115--138},
issn = {0004-5411},
mrclass = {03F20},
mrnumber = {2145651},
mrreviewer = {G. E. Mints},
doi = {10.1145/972639.972640},
zblnumber = {1063.03044},
} -
[bobo] A. A. Razborov, "Bounded arithmetic and lower bounds in Boolean complexity," in Feasible Mathematics, II, Boston: Birkhäuser, 1995, vol. 13, pp. 344-386.
@incollection{bobo, mrkey = {1322282},
author = {Razborov, Alexander A.},
title = {Bounded arithmetic and lower bounds in {B}oolean complexity},
booktitle = {Feasible Mathematics, {II}},
venue = {{I}thaca, {NY},
1992},
series = {Progr. Comput. Sci. Appl. Logic},
volume = {13},
pages = {344--386},
publisher = {Birkhäuser},
address = {Boston},
year = {1995},
mrclass = {03D15 (03F30 06E30 68Q15)},
mrnumber = {1322282},
mrreviewer = {Shih Ping Tung},
zblnumber = {0838.03044},
} -
[ind]
A. A. Razborov, "Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic," Izv. Ross. Akad. Nauk Ser. Mat., vol. 59, iss. 1, pp. 201-224, 1995.
@article{ind, mrkey = {1328561},
author = {Razborov, Alexander A.},
title = {Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic},
journal = {Izv. Ross. Akad. Nauk Ser. Mat.},
fjournal = {Rossiĭskaya Akademiya Nauk. Izvestiya. Seriya Matematicheskaya},
volume = {59},
year = {1995},
number = {1},
pages = {201--224},
issn = {0373-2436},
mrclass = {03D15 (03F30 03F35 68Q15)},
mrnumber = {1328561},
mrreviewer = {Alessandro Berarducci},
doi = {10.1070/IM1995v059n01ABEH000009},
} -
[icalp]
A. A. Razborov, "Lower bounds for propositional proofs and independence results in bounded arithmetic," in Automata, Languages and Programming, New York: Springer-Verlag, 1996, vol. 1099, pp. 48-62.
@incollection{icalp, mrkey = {1464440},
author = {Razborov, Alexander A.},
title = {Lower bounds for propositional proofs and independence results in bounded arithmetic},
booktitle = {Automata, Languages and Programming},
venue = {{P}aderborn, 1996},
series = {Lecture Notes in Comput. Sci.},
volume = {1099},
pages = {48--62},
publisher = {Springer-Verlag},
year = {1996},
mrclass = {03F20 (03F30 68Q15 68Q25)},
mrnumber = {1464440},
doi = {10.1007/3-540-61440-0_116},
address = {New York},
zblnumber = {1045.03524},
} -
[polynom]
A. A. Razborov, "Lower bounds for the polynomial calculus," Comput. Complexity, vol. 7, iss. 4, pp. 291-324, 1998.
@article{polynom, mrkey = {1691494},
author = {Razborov, Alexander A.},
title = {Lower bounds for the polynomial calculus},
journal = {Comput. Complexity},
fjournal = {Computational Complexity},
volume = {7},
year = {1998},
number = {4},
pages = {291--324},
issn = {1016-3328},
coden = {CPTCEU},
mrclass = {03F20 (03D15 13P10 68Q15)},
mrnumber = {1691494},
mrreviewer = {Søren M. Riis},
doi = {10.1007/s000370050013},
zblnumber = {1026.03043},
} -
[php_survey] A. A. Razborov, "Proof complexity of pigeonhole principles," in Developments in Language Theory, New York: Springer-Verlag, 2002, vol. 2295, pp. 110-116.
@incollection{php_survey, mrkey = {1964164},
author = {Razborov, Alexander A.},
title = {Proof complexity of pigeonhole principles},
booktitle = {Developments in Language Theory},
venue = {{V}ienna, 2001},
series = {Lecture Notes in Comput. Sci.},
volume = {2295},
pages = {110--116},
publisher = {Springer-Verlag},
year = {2002},
mrclass = {03F20 (03D15 68Q15 68Q17)},
mrnumber = {1964164},
address = {New York},
zblnumber = {1073.03540},
} -
[matching]
A. A. Razborov, "Resolution lower bounds for perfect matching principles," J. Comput. System Sci., vol. 69, iss. 1, pp. 3-27, 2004.
@article{matching, mrkey = {2070797},
author = {Razborov, Alexander A.},
title = {Resolution lower bounds for perfect matching principles},
journal = {J. Comput. System Sci.},
fjournal = {Journal of Computer and System Sciences},
volume = {69},
year = {2004},
number = {1},
pages = {3--27},
issn = {0022-0000},
coden = {JCSSBM},
mrclass = {03F20 (05D15 68Q17)},
mrnumber = {2070797},
mrreviewer = {Jan Kraj{\'ı}{\v{c}}ek},
doi = {10.1016/j.jcss.2004.01.004},
zblnumber = {1106.03049},
} -
[int]
A. A. Razborov and S. Rudich, "Natural proofs," J. Comput. System Sci., vol. 55, iss. 1, part 1, pp. 24-35, 1997.
@article{int, mrkey = {1473047},
author = {Razborov, Alexander A. and Rudich, Steven},
title = {Natural proofs},
journal = {J. Comput. System Sci.},
fjournal = {Journal of Computer and System Sciences},
volume = {55},
year = {1997},
number = {1, part 1},
pages = {24--35},
issn = {0022-0000},
coden = {JCSSBM},
mrclass = {68Q15 (68Q10 68Q25 94C10)},
mrnumber = {1473047},
mrreviewer = {Juraj Hromkovi{\v{c}}},
doi = {10.1006/jcss.1997.1494},
zblnumber = {0884.68055},
} -
[SBI]
N. Segerlind, S. Buss, and R. Impagliazzo, "A switching lemma for small restrictions and lower bounds for $k$-DNF resolution," SIAM J. Comput., vol. 33, iss. 5, pp. 1171-1200, 2004.
@article{SBI, mrkey = {2084484},
author = {Segerlind, Nathan and Buss, Sam and Impagliazzo, Russell},
title = {A switching lemma for small restrictions and lower bounds for {$k$}-{DNF} resolution},
journal = {SIAM J. Comput.},
fjournal = {SIAM Journal on Computing},
volume = {33},
year = {2004},
number = {5},
pages = {1171--1200},
issn = {0097-5397},
mrclass = {03F20 (68Q15)},
mrnumber = {2084484},
mrreviewer = {Jan Kraj{\'ı}{\v{c}}ek},
doi = {10.1137/S0097539703428555},
zblnumber = {1059.03063},
} -
[Urq2]
A. Urquhart, "The complexity of propositional proofs," Bull. Symbolic Logic, vol. 1, iss. 4, pp. 425-467, 1995.
@article{Urq2, mrkey = {1369171},
author = {Urquhart, Alasdair},
title = {The complexity of propositional proofs},
journal = {Bull. Symbolic Logic},
fjournal = {The Bulletin of Symbolic Logic},
volume = {1},
year = {1995},
number = {4},
pages = {425--467},
issn = {1079-8986},
mrclass = {03F20 (03B05 03B35 03D15 03F05 68T15)},
mrnumber = {1369171},
mrreviewer = {G. Asser},
doi = {10.2307/421131},
zblnumber = {0845.03025},
} -
[Yao4]
A. C. Yao, "Theory and applications of trapdoor functions," in 23rd Annual Symposium on Foundations of Computer Science, New York: IEEE, 1982, pp. 80-91.
@incollection{Yao4, mrkey = {0780384},
author = {Yao, Andrew C.},
title = {Theory and applications of trapdoor functions},
booktitle = {23rd Annual Symposium on Foundations of Computer Science},
venue = {{C}hicago, {I}ll., 1982},
pages = {80--91},
publisher = {IEEE},
address = {New York},
year = {1982},
mrclass = {68Q30 (68Q15)},
mrnumber = {0780384},
doi = {10.1109/SFCS.1982.45},
}