[1]   Miklós Ajtai: The complexity of the pigeonhole principle. Combinatorica, 14(4):417–433, 1994. Preliminary version in FOCS’88. [doi:10.1007/BF01302964]

[2]   Yaroslav Alekseev: A lower bound for polynomial calculus with extension rule. In Proc. 36th Comput. Complexity Conf. (CCC’21), pp. 21:1–18. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2021. [doi:10.4230/LIPIcs.CCC.2021.21]

[3]   Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch, and Iddo Tzameret: Semialgebraic proofs, IPS lower bounds, and the τ-conjecture: Can a natural number be negative? SIAM J. Comput., 53(3):648–700, 2024. Preliminary version in STOC’20. [doi:10.1137/20M1374523]

[4]   Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák: Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proc. London Math. Soc., 73(1):1–26, 1996. [doi:10.1112/plms/s3-73.1.1]

[5]   Stephen Bellantoni, Toniann Pitassi, and Alasdair Urquhart: Approximation and small-depth Frege proofs. SIAM J. Comput., 21(6):1161–1179, 1992. [doi:10.1137/0221068]

[6]   Sam Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi: Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. System Sci., 62(2):267–289, 2001. [doi:10.1006/jcss.2000.1726]

[7]   Samuel R. Buss, Russell Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiří Sgall: Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Comput. Complexity, 6(3):256–298, 1996. [doi:10.1007/BF01294258]

[8]   Vašek Chvátal, William J. Cook, and Mark E. Hartmann: On cutting-plane proofs in combinatorial optimization. Lin. Alg. Appl., 114–115:455–499, 1989. [doi:10.1016/0024-3795(89)90476-X]

[9]   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]

[10]   Stephen A. Cook and Robert A. Reckhow: The relative efficiency of propositional proof systems. J. Symbolic Logic, 44(1):36–50, 1979. This is a journal version of Cook–Reckhow, STOC’74 and Reckhow’s 1976 PhD Thesis (U. Toronto). [doi:10.2307/2273702]

[11]   William J. Cook, Collette R. Coullard, and György Turán: On the complexity of cutting plane proofs. Discr. Appl. Math., 18(1):25–38, 1987. [doi:10.1016/0166-218X(87)90039-4]

[12]   Noah Fleming, Pravesh Kothari, and Toniann Pitassi: Semialgebraic proofs and efficient algorithm design. Found. Trends Theor. Comp. Sci., 14(1–2):1–221, 2019. [doi:10.1561/0400000086, ECCC:TR19-106]

[13]   Dima Grigoriev and Edward A. Hirsch: Algebraic proof systems over formulas. Theoret. Comput. Sci., 303(1):83–102, 2003. [doi:doi:10.1016/S0304-3975(02)00446-2]

[14]   Joshua A. Grochow and Toniann Pitassi: Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system. J. ACM, 65(6):37:1–59, 2018. [doi:10.1145/3230742]

[15]   Armin Haken: The intractability of resolution. Theoret. Comput. Sci., 39(2–3):297–308, 1985. [doi:10.1016/0304-3975(85)90144-6]

[16]   Tuomas Hakoniemi: Monomial size vs. bit-complexity in Sums-of-Squares and Polynomial Calculus. In Proc. 36th Ann. ACM/IEEE Symp. on Logic in Computer Science (LICS’21), pp. 55:1–7. ACM Press, 2021. [doi:10.1109/LICS52264.2021.9470545]

[17]   Johan Håstad: On small-depth Frege proofs for Tseitin for grids. J. ACM, 68(1):1:1–31, 2020. [doi:10.1145/3425606]

[18]   Russell Impagliazzo, Sasank Mouli, and Toniann Pitassi: The surprising power of constant depth algebraic proofs. In Proc. 35th Ann. ACM/IEEE Symp. on Logic in Computer Science (LICS’20), pp. 591–603. ACM Press, 2020. [doi:10.1145/3373718.3394754]

[19]   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]

[20]   Dmitry Itsykson and Dmitry Sokolov: Resolution over linear equations modulo two. Ann. Pure Appl. Logic, 171(1):102722:1–31, 2020. [doi:10.1016/j.apal.2019.102722]

[21]   Jan Krajíček: Discretely ordered modules as a first-order extension of the cutting planes proof system. J. Symbolic Logic, 63(4):1582–1596, 1998. [doi:10.2307/2586668]

[22]   Jan Krajíček and Pavel Pudlák: Propositional proof systems, the consistency of first order theories and the complexity of computations. J. Symbolic Logic, 54(3):1063–1079, 1989. [doi:10.2307/2274765]

[23]   Ryan O’Donnell: SOS is not obviously automatizable, even approximately. In Proc. 8th Innovations in Theoret. Comp. Sci. Conf. (ITCS’17), pp. 59:1–10. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2017. [doi:10.4230/LIPIcs.ITCS.2017.59]

[24]   Fedor Part and Iddo Tzameret: Resolution with counting: Dag-like lower bounds and different moduli. Comput. Complexity, 30(2):1–71, 2021. Preliminary version in ITCS’20. [doi:10.1007/s00037-020-00202-x]

[25]   Toniann Pitassi: Algebraic propositional proof systems. In Neil Immerman and Phokion Kolaitis, editors, Descriptive Complexity and Finite Models, volume 31 of DIMACS Ser. Discrete Math. Theoret. Comput. Sci., pp. 215–244. Amer. Math. Soc., 1997.

[26]   Toniann Pitassi: Unsolvable systems of equations and proof complexity. In Proc. Internat. Congress of Mathematicians, Vol. III (Berlin, 1998), pp. 451–460. Documenta Mathematica, 1998. Accessible at EMS Press.

[27]   Toniann Pitassi and Rahul Santhanam: Effectively polynomial simulations. In Proc. 1st Innovations in Comp. Sci. Conf. (ICS’10), pp. 370–382. Tsinghua U., 2010. Accessible at Tsinghua U.

[28]   Prasad Raghavendra and Benjamin Weitz: On the bit complexity of Sum-of-Squares proofs. In Proc. 44th Internat. Colloq. on Automata, Languages, and Programming (ICALP’17), pp. 80:1–13. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2017. [doi:10.4230/LIPIcs.ICALP.2017.80]

[29]   Ran Raz and Iddo Tzameret: Resolution over linear equations and multilinear proofs. Ann. Pure Appl. Logic, 155(3):194–224, 2008. [doi:10.1016/j.apal.2008.04.001]

[30]   Alexander A. Razborov: Lower bounds on the size of bounded depth circuits over a complete basis with logical addition. Math. Notes. Acad. Sci. USSR (English translation), 41(4):333–338, 1987. [doi:10.1007/BF01137685]

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

[32]   Roman Smolensky: Algebraic methods in the theory of lower bounds for Boolean circuit complexity. In Proc. 19th STOC, pp. 77–82. ACM Press, 1987. [doi:10.1145/28395.28404]

[33]   Dmitry Sokolov: (Semi)algebraic proofs over ±1 variables. In Proc. 52nd STOC, pp. 78–90. ACM Press, 2020. [doi:10.1145/3357713.3384288]

[34]   Grigori S. Tseitin: On the complexity of derivations in propositional calculus. Studies in constructive mathematics and mathematical logic Part II. Consultants Bureau, New-York-London, 1968. Reproduced in Automation of Reasoning, Springer, 1983.