[1]   Albert Atserias and Victor 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]

[2]   Albert Atserias, Massimo Lauria, and Jakob Nordström: Narrow proofs may be maximally long. ACM Trans. Comput. Logic, 17(3):19:1–19:30, 2016. Preliminary version in CCC’14. [doi:10.1145/2898435, arXiv:1409.2731]

[3]   Arnold Beckmann, Pavel Pudlák, and Neil Thapen: Parity games and propositional proofs. ACM Trans. Comput. Logic, 15(2):17:1–17:30, 2014. Preliminary versions in MFCS’13 and ECCC. [doi:10.1145/2579822]

[4]   Eli Ben-Sasson: Size-space tradeoffs for resolution. SIAM J. Comput., 38(6):2511–2525, 2009. Preliminary version in STOC’02. [doi:10.1137/080723880]

[5]   Eli Ben-Sasson and Jakob Nordström: Understanding space in proof complexity: Separations and trade-offs via substitutions (extended abstract). In Proc. 2nd Symp. on Innovations in Comput. Sci. (ICS’11), pp. 401–416, 2011. Available at ICS and ECCC. [arXiv:1008.1789]

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

[7]   Samuel Buss: Bounded Arithmetic. Bibliopolis, 1986.

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

[9]   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–28:15, 2015. Preliminary version in STACS’14. [doi:10.1145/2746339, arXiv:1409.2978]

[10]   David S. Johnson, Christos H. Papadimitriou, and Mihalis Yannakakis: How easy is local search? J. Comput. System Sci., 37(1):79–100, 1988. Preliminary version in FOCS’85. [doi:10.1016/0022-0000(88)90046-3]

[11]   Jan Krajíček: On the weak pigeonhole principle. Fundamenta Math., 170(1-2):123–140, 2001. [doi:10.4064/fm170-1-8]

[12]   Jan Krajíček, Alan Skelley, and Neil Thapen: NP search problems in low fragments of bounded arithmetic. J. Symbolic Logic, 72(2):649–672, 2007. [doi:10.2178/jsl/1185803628]

[13]   Jakob Nordström: A simplified way of proving trade-off results for resolution. Inform. Process. Lett., 109(18):1030–1035, 2009. [doi:10.1016/j.ipl.2009.06.006]

[14]   Jakob Nordström: Pebble games, proof complexity and time-space trade-offs. Logical Methods in Comput. Sci., 9(3):15:1–15:63, 2013. [doi:10.2168/lmcs-9(3:15)2013, arXiv:1307.3913]

[15]   Jakob Nordström and Johan Håstad: Towards an optimal separation of space and length in resolution. Theory of Computing, 9(14):471–557, 2013. Preliminary versions in STOC’08 and ECCC. [doi:10.4086/toc.2013.v009a014, arXiv:0803.0661]

[16]   Pavel Pudlák: Proofs as games. Amer. Math. Monthly, 107(6):541–550, 2000. [doi:10.2307/2589349]

[17]   Alexander Razborov: A new kind of tradeoffs in propositional proof complexity. J. ACM, 63(2):16:1–16:14, 2016. Available at author’s website. [doi:10.1145/2858790]

[18]   Alan Skelley and Neil Thapen: The provably total search problems of bounded arithmetic. Proc. London Math. Soc., 103(1):106–138, 2011. [doi:10.1112/plms/pdq044]