[1]   Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson: Space complexity in propositional calculus. SIAM J. Comput., 31(4):1184–1211, 2002. Preliminary version in STOC’00. [doi:10.1137/S0097539700366735]

[2]   Michael Alekhnovich and Alexander A. Razborov: Lower bounds for polynomial calculus: Non-binomial case. Proc. Steklov Inst. Math., 242:18–35, 2003. Available at Math-Net.Ru (Russian with English home page) and at author’s home page (English). Preliminary version in FOCS’01.

[3]   Albert Atserias and Víctor Dalmau: A combinatorial characterization of resolution width. J. Comput. System Sci., 74(3):323–334, 2008. Preliminary version in CCC’03. [doi:10.1016/j.jcss.2007.06.025]

[4]   Per Austrin and Kilian Risse: Perfect matching in random graphs is as hard as Tseitin. TheoretiCS, 1(2):1–47, 2022. Preliminary version in SODA’22. [doi:10.46298/theoretics.22.2]

[5]   Eli Ben-Sasson and Nicola Galesi: Space complexity of random formulae in resolution. Random Struct. Algor., 23(1):92–109, 2003. Preliminary version in CCC’01. [doi:10.1002/rsa.10089]

[6]   Eli Ben-Sasson and Avi Wigderson: Short proofs are narrow—resolution made simple. J. ACM, 48(2):149–169, 2001. Preliminary version in STOC’99. [doi:10.1145/375827.375835]

[7]   Christoph Berkholz and Jakob Nordström: Supercritical space-width trade-offs for resolution. SIAM J. Comput., 49(1):98–118, 2020. Preliminary version in ICALP’16. [doi:10.1137/16M1109072]

[8]   Ilario Bonacina: Total space in resolution is at least width squared. In Proc. 43rd Internat. Colloq. on Automata, Languages, and Programming (ICALP’16), pp. 56:1–13. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016. [doi:10.4230/LIPIcs.ICALP.2016.56]

[9]   Ilario Bonacina and Nicola Galesi: A framework for space complexity in algebraic proof systems. J. ACM, 62(3):23:1–20, 2015. Preliminary version in ITCS’13. [doi:10.1145/2699438]

[10]   Ilario Bonacina, Nicola Galesi, and Neil Thapen: Total space in resolution. SIAM J. Comput., 45(5):1894–1909, 2016. Preliminary version in FOCS’14. [doi:10.1137/15M1023269]

[11]   Maria Luisa Bonet and Nicola Galesi: Optimality of size-width tradeoffs for resolution. Comput. Complexity, 10(4):261–276, 2001. [doi:10.1007/s000370100000]

[12]   Sam Buss: Axiomatizations and conservation results for fragments of bounded arithmetic. In Wilfried Sieg, editor, Logic and Computation, volume 106, pp. 57–84, 1990. [doi:10.1090/conm/106/1057816]

[13]   Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo: Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proc. 28th STOC, pp. 174–183. ACM Press, 1996. [doi:10.1145/237814.237860]

[14]   Stephen A. Cook and Robert A. Reckhow: The relative efficiency of propositional proof systems. J. Symbolic Logic, 44(1):36–50, 1979. Preliminary version in STOC’74. [doi:10.2307/2273702]

[15]   Juan Luis Esteban and Jacobo Torán: Space bounds for resolution. Inform. Comput., 171(1):84–97, 2001. Preliminary version in STACS’99 and CSL’99. [doi:10.1006/inco.2001.2921]

[16]   Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals: From small space to small width in resolution. ACM Trans. Comput. Logic, 16(4):28:1–15, 2015. Preliminary version in STACS’14. [doi:10.1145/2746339]

[17]   Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals: Towards an understanding of polynomial calculus: New separations and lower bounds. Theory of Computing, 21(4):1–48, 2025. Preliminary version in ICALP’13. [doi:10.4086/toc.2025.v021a004]

[18]   Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, and Neil Thapen: Space complexity in polynomial calculus. SIAM J. Comput., 44(4):1119–1153, 2015. Preliminary version in CCC’12. [doi:10.1137/120895950]

[19]   Nicola Galesi, Leszek Aleksander Kołodziejczyk, and Neil Thapen: Polynomial calculus space and resolution width. In Proc. 60th FOCS, pp. 1325–1337. IEEE Comp. Soc., 2019. [doi:10.1109/FOCS.2019.00081]

[20]   Nicola Galesi and Massimo Lauria: On the automatizability of polynomial calculus. Theory Computing Sys., 47(2):491–506, 2010. [doi:10.1007/s00224-009-9195-5]

[21]   Nicola Galesi and Massimo Lauria: Optimality of size-degree tradeoffs for polynomial calculus. ACM Trans. Comput. Logic, 12(1):4:1–22, 2010. [doi:10.1145/1838552.1838556]

[22]   Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall: Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Comput. Complexity, 8(2):127–144, 1999. [doi:10.1007/s000370050024]

[23]   Dmitry Itsykson, Vsevolod Oparin, Mikhail Slabodkin, and Dmitry Sokolov: Tight lower bounds on the resolution complexity of perfect matching principles. Fundam. Informaticae, 145(3):229–242, 2016. [doi:10.3233/FI-2016-1358]

[24]   Leszek Aleksander Kołodziejczyk and Neil Thapen: Approximate counting and NP search problems. J. Math. Logic, 22(3):2250012:1–31, 2022. [doi:10.1142/S021906132250012X]

[25]   Jan Krajíček, Pavel Pudlák, and Alan Woods: An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Struct. Algor., 7(1):15–39, 1995. Preliminary version in STOC’92. [doi:10.1002/rsa.3240070103]

[26]   Mladen Mikša and Jakob Nordström: A generalized method for proving polynomial calculus degree lower bounds. J. ACM, 71(6/37):1–43, 2024. Preliminary version in CCC’15. [doi:10.1145/3675668]

[27]   Jakob Nordström: On the interplay between proof complexity and SAT solving. ACM SIGLOG News, 2(3):19–44, 2015. [doi:10.1145/2815493.2815497]

[28]   Toniann Pitassi, Paul Beame, and Russell Impagliazzo: Exponential lower bounds for the pigeonhole principle. Comput. Complexity, 3:97–140, 1993. Preliminary version in STOC’92. See also author’s home page. [doi:10.1007/BF01200117]

[29]   Pavel Pudlák and Neil Thapen: Random resolution refutations. Comput. Complexity, 28(2):185–239, 2019. Preliminary version in CCC’17. [doi:10.1007/s00037-019-00182-7]

[30]   Alexander A. Razborov: Lower bounds for the polynomial calculus. Comput. Complexity, 7(4):291–324, 1998. [doi:10.1007/s000370050013]

[31]   Alexander A. Razborov: Proof complexity of pigeonhole principles. In Proc. 5th Internat. Conf. on Developments in Language Theory (DLT’01), pp. 100–116, 2001. [doi:10.1007/3-540-46011-X_8]

[32]   Alexander A. Razborov: Resolution lower bounds for the weak functional pigeonhole principle. Theoret. Comput. Sci., 303(1):233–243, 2003. [doi:10.1016/S0304-3975(02)00453-X]

[33]   Søren Riis: Independence in Bounded Arithmetic. Ph. D. thesis, The University of Oxford, 1993. LINK: Google Books.

[34]   Nathan Segerlind, Samuel R. Buss, and Russell Impagliazzo: A switching lemma for small restrictions and lower bounds for k-DNF resolution. SIAM J. Comput., 33(5):1171–1200, 2004. Preliminary version in FOCS’02. [doi:10.1137/S0097539703428555]

[35]   Alasdair Urquhart: Hard examples for resolution. J. ACM, 34(1):209–219, 1987. [doi:10.1145/7531.8928]