Jan Krajicek' bibliography

The published papers may differ in print from the files (ps, compressed ps or pdf) available here by changes done in page proofs. The copyrights are generally with the publishers; hence the papers should be downloaded for personal use only.

Research papers (and the most recent),
expository papers (and the most recent ),
old lecture notes,
books and
edited volumes.

Starting with 2012 I send all preprints to the ArXiv archive.
(orcid id)

(For printing the files it may be necessary sometimes to specify the paper size as A4; e.g., in ghostview this can be done in menu choice "media".)

Thesis and habilitations

---

• RNDr.Thesis: "Non-classical Foundations of Mathematics", in Czech, Charles University, April 1985.
  
  
• CSc.Habilitation: "Complexity of Formal Proofs", a collection of five papers (in English) with an introduction and overview (in Czech), Academy of Sciences, September 1989.
  
  
• DrSc.Habilitation: "Bounded Arithmetic, Propositional Calculus, and Complexity Theory", a collection of ten papers (in English) with an introduction and overview (in Czech), Academy of Sciences, August 1992.
  
  
• Doc.Habilitation: "Lower bounds in propositional calculus and independence results in bounded arithmetic", a collection of twelve papers (in English) with an introduction and overview (in Czech), Charles University, May 2000.

Abstracts and extended abstracts - selected

---

• "Some Theorems on the Lattice of Local Interpretability Types" (abstract), Commentationes Mathematicae Universitas Carolinae, 24(2), (1983), p. 387.
  
  
• "A Possible Modal Reformulation of Comprehension Scheme" (abstract), Commentationes Mathematicae Universitas Carolinae, 24(2), (1983), pp. 387-388.
  
  
• "Measures of Complexity of Proofs" (extended abstract), Abstracts of $8^{\mbox{th}}$ Inter. Congress on Logic, Methodology and Philosophy of Science '87, Moscow, August 1987, Vol. 5, Part 1, pp. 151-154.
  
  
• "Three Theorems on Bounded Arithmetic" (abstract), Annual 1989 Meeting of ASL at Los Angeles, J. Symbolic Logic, 55(1), pp.377-378.
  
  
• with P. Beame, R. Impagliazzo, T. Pitassi, P.Pudl\'{a}k and A. Woods: "Exponential Lower Bound for the Pigeonhole Principle" (extended abstract), in: Proc. ACM Symp. on Theory of Computing, ACM Press, (1992), pp.200-220.
  
  
• "Problems of complexity theory in models of bounded arithmetic" (extended abstract), in: {\em Proof Theory, Complexity and Metamathematics}, Technological University of Vienna and Kurt Godel Society, (1994).
  
  
• "A non-conservation result for bounded arithmetic and search problems" (abstract), in: {\em Proof Theory, Complexity and Metamathematics}, Technological University of Vienna and Kurt Godel Society, (1994).
  
  
• with P. Beame, R. Impagliazzo, T. Pitassi and P.Pudl\'{a}k: "Lower bounds on Hilbert's Nullstellensatz and propositional proofs" (extended abstract), in: Proc. IEEE 35$^{\mbox{th}}$ Annual Symp. on Foundation of Computer Science, (1994), pp.794-806.
  
  
• "Valuations of Boolean formulae in partial algebras", in: Volume of Abstracts of the Tenth International Congress {\em Logic, Methodology and Philosophy of Science}, International Union of History and Philosophy of Science, Florence (August 19-25, 1995), (1995), pp.6-7.
  
  
• "Propositional proofs, proofs of membership in polynomial ideals, and their complexity", in: Abstracts of the annual European meeting of the Association of Symbolic Logic, {\em Logic Colloquium 95}, Haifa (August 9-17, 1995), (1995), p.PROOF-22. Also in: {\em Bulletin of the ASL}, {\bf 3(1)}, (1997), pp.77-78.
  
  
• "Classical propositional logic and its complexity", a syllabus and references for an advanced logic course given at the {\em Eight European Summer School in Logic, Language and Information} held in Prague, August 12-23, 1996.
  Available online.
  
  
• ``Bounded arithmetic, propositional logic, and complexity theory'', in: Proc. of the bi-annual meeting of the Japanese Mathematical Society, Tokyo, September 1997.
  
  
• ``Effective interpolation'', a syllabus and references for a course given at the Tohoku University in Sendai (Japan), October 2-4, 1997.
  Available online.
  
  
• "Forcing with random variables and proof complexity", eds. A.Beckmann, U.Berger, B.Löwe, and J.V.Tucker: Logical Approaches to Computational Barriers, 2nd Conference on Computability in Europe, CiE 2006, Swansea, UK, July 2006, Lecture Notes in Computer Science, Springer, (2006), pp.277-278. Pdf file.
  
  
• Proof search problem (ext.abstract)
  in: Mathematical Logic: Proof Theory, Constructive Mathematics (9.-13.11.2020),
  Oberwolfach Reports (OWR), Report No. 34/2020, (2020), pp.45-46.
  DOI, slides.

Expository papers

---

• "Modal Set Theory", Proc. $2^{\mbox{nd}}$ Easter Conference on Model Theory, Wittenberg 1984, in: Seminarberichte Nr. 60, Humboldt Univ., Berlin, (1984), pp. 87-99.
  
  
• "Generalizations of Proofs", Proc. $5^{\mbox{th}}$ Easter Conf. on Model Theory, Wendisch-Rietz 1987, in: Seminarberichte Nr. 93, Humboldt University, Berlin, (1987), pp. 82-99.
  
  
• with P. Clote: "Open Problems", in: "Arithmetic, Proof Theory and Computational Complexity", eds. P. Clote and J. Kraj\'{\i}\v{c}ek, Oxford Press, (1993), pp.1-19.
  
  
• "A fundamental problem of mathematical logic", Annals of the Kurt G\"{o}del Society, Springer-Verlag, Collegium Logicum, Vol.2, (1996), pp.56-64. ISBN 3-211-82796-X.
  
  
• "On methods for proving lower bounds in propositional logic", in: {\em Logic and Scientific Methods} Eds. M. L. Dalla Chiara et al., (Vol. 1 of Proc. of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence (August 19-25, 1995)), Synthese Library, Vol.259, Kluwer Academic Publ., Dordrecht, (1997), pp.69-83.
  Pdf.
  
  
• ``Boolean circuits'', in: {\em Encyclopaedia of Mathematics}, ed.M.~Hazelwinkel, Kluwer Academic Publ., (2000), pp.79-80.
  
  
• "Hardness assumptions in the foundations of theoretical computer science", Archive for Mathematical Logic, 44(6)}, (2005), pp.667-675.
  Pdf file.
  
  
• Proof complexity, in: Laptev, A. (ed.), European congress of mathematics (ECM), Stockholm, Sweden, June 27--July 2, 2004. Zurich: European Mathematical Society, (2005), pp.221-231. Pdf file.
  
  
• "From feasible proofs to feasible computations", in: Computer Science Logic 2010, A. Dawar and H. Veith (Eds.), LNCS 6247, Springer, Heidelberg (2010), pp.22-31. Pdf file.
  
  
• Expansions of pseudofinite structures and circuit and proof complexity,
  in: Liber Amicorum Alberti, eds.Jan van Eijck, Rosalie Iemhoff and Joost J. Joosten, Tributes Ser. Vol.30, College Publications, London, (2016), pp.195-203.
  ISBN 978-1-84890-204-6
  ArXiv/abstr, pdf and ps.
  
  
• The Cook-Reckhow definition,
  preliminary version, Sept. 2019,
  (for the ACM A.M.Turing Award winners book series).
  ArXiv/abstr..

Research papers

---

• Some Theorems on the Lattice of Local Interpretability Types, Zeitschr. f. Mathematikal Logik u. Grundlagen d. Mathematik, Bd. 31, (1985), pp. 449-460.
  
  
• "A Possible Modal Formulation of Comprehension Scheme", Zeitchr. f. Mathematikal Logik u. Grundlagen d. Mathematik, Bd. 33(5), (1987), pp. 461-480.
  
  
• "Some Results and Problems in the Modal Set Theory MST", Zeitschr. f. Mathematikal Logik u. Grundlagen d. Mathematik, Bd. 34(2), (1988), pp.123-134.
  
  
• "A Note of Proofs of Falsehood", Archiv f. Mathematikal Logik u. Grundlagen 26 (3-4), (1987), pp. 169-179.
  
  
• "On the Number of Steps in Proofs", Annals of Pure and Applied Logic 41(2), (1989), pp. 153-178.
  
  
• with P. Pudl\'{a}k: "The Number of Proof Lines and the Size of Proofs in First Order Logic", Archive for Mathematical Logic 27, (1988), pp. 69-84.
  
  
• with P. Pudl\'{a}k: "Propositional Proof Systems, the Consistency of First Order Theories and the Complexity of Computations", J. Symbolic Logic, 54(3), (1989), pp. 1063-1079.
  
  
• with P. Pudl\'{a}k: "Quantified Propositional Calculi and Fragments of Bounded Arithmetic", Zeitschr. f. Mathematikal Logik u. Grundlagen d. Mathematik, Bd. 36(1), (1990), pp. 29-46.
  
  
• "A Theorem on Uniform Provability of Schemes", Proc. $6^{\mbox{th}}$ Easter Conf. on Model Theory, Wendisch-Rietz 1988, in: Seminarberichte Nr. 98, Humboldt Univ., Berlin, (1988), pp. 85-92.
  
  
• with P. Pudl\'{a}k: "On the Structure of Initial Segments of Models of Arithmetic", Archive for Mathematical Logic, 28(2), (1989), pp, 91-98.
  
  
• "$\Pi_1$-Conservativeness in Systems of Bounded Arithmetic", unpublished typescript.
  
  
• "Speed-up for Propositional Frege Systems via Generalizations of Proofs", Commentationes Mathematicae Universitas Carolinae, 30(1), (1989), pp.137-140.
  
  
• "Exponentiation and Second Order Bounded Arithmetic", Annals of Pure and Applied Logic, 48(3), (1990), pp. 261-276.
  
  
• with P. Pudl\'{a}k and G. Takeuti: "Bounded Arithmetic and the Polynomial Hierarchy", Annals of Pure and Applied Logic, 52, (1991), pp. 143-153.
  
  
• with G. Takeuti: "On Bounded $\sum^1_1$-Polynomial Induction", in: Feasible Mathematics, eds. S.R. Buss and P.J. Scott, (1990), Birkhauser, pp. 259-280.
  
  
• with P. Pudl\'{a}k: "Propositional Provability and Models of Weak Arithmetic", in: Computer Science Logic (Kaiserlautern, Oct. '89), E. Borger, H. Kleine Buning, M.M. Richter (eds.), LNCS 440, (1990), Springer-Verlag, pp. 193-210.
  
  
• with G. Takeuti: "On Induction-Free Provability", Annals of Mathematics and Artificial Intelligence, 6, (1992), pp.107-126.
  
  
• "No Counter-Example Interpretation and Interactive Computation", in: "Logic from Computer Science", ed. Y.N. Moschovakis, Mathematical Sciences Research Institute Publ. 21, Berkeley, Springer-Verlag, (1992), pp. 287-293.
  
  
• with P. Pudl\'{a}k and J. Sgall: "Interactive Computations of Optimal Solutions", in: B. Rovan (ed.): Mathematical Foundations of Computer Science (B. Bystrica, August '90), Lecture Notes in Computer Science 452, Springer-Verlag, (1990), pp. 48-60.
  
  
• "Fragments of Bounded Arithmetic and Bounded Query Classes", Transactions of the AMS, 338(2), (1993), pp.587-598.
  
  
• with S. Buss: "An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic", Proceedings of the London Mathematical Society, 69(3), (1994), pp.1-21.
  
  
• with S. Buss and G. Takeuti: "Provably Total Functions in Bounded Arithmetic Theories $R^i_3, U^i_2$ and $V^i_2$", in: "Arithmetic, Proof Theory and Computational Complexity", eds. P. Clote and J. Kraj\'{\i}\v{c}ek, Oxford Press, (1993), pp.116-161. Pdf.
  
  
• "Lower Bounds to the Size of Constant-Depth Propositional Proofs", J. of Symbolic Logic, 59(1), (1994), pp.73-86.
  
  
• with P. Pudl\'{a}k and A. Woods: "An Exponential Lower Bound to the Size of Bounded Depth Frege Proofs of the Pigeonhole principle", Random Structures and Algorithms, 7(1), (1995), pp.15-39.
  Appeared also in the Electronic Colloquium on Computational Complexity, Report nr.: TR94-018.
  
  
• "On Frege and Extended Frege Proof Systems", in: "Feasible Mathematics II", eds. P. Clote and J. Remmel, Birkhauser, (1995), pp. 284-319.
  
  
• with P. Beame, R. Impagliazzo, T. Pitassi and P.Pudl\'{a}k: "Lower bounds on Hilbert's Nullstellensatz and propositional proofs", Proceedings of the London Mathematical Society, {\bf (3) 73}, (1996), pp.1-26.
  
  
• with M. Chiari : "Witnessing functions in bounded arithmetic and search problems", J. of Symbolic Logic, {\bf 63(3)}, (1998), pp. 1095-1115.
  
  
• "Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic", J. of Symbolic Logic, {\bf 62(2)}, (1997), pp.457-486.
  
  
• with P. Pudl\'{a}k: "Some consequences of cryptographical conjectures for $S^1_2$ and $EF$", in: {\em Logic and Computational Complexity} (Proc. of the meeting held in Indianapolis, October 1994), Ed. D. Leivant, Springer-Verlag, Lecture Notes in Computer Science, Vol. {\bf 960}, (1995), pp.210-220.
  Revised version in: {\em Information and Computation}, Vol. {\bf 140 (1)}, (January 10, 1998), pp.82-94.
  
  
• with S. Buss, R. Impagliazzo, P. Pudl\'{a}k, A. A. Razborov and J. Sgall: "Proof complexity in algebraic systems and bounded depth Frege systems with modular counting", {\em Computational Complexity}, {\bf 6(3)}, 1996/1997, pp.256-298.
  
  
• "Extensions of models of $PV$", in: Logic Colloquium'95, Eds. J.A.Makowsky and E.V.Ravve, ASL/Springer Series {\em Lecture Notes in Logic}, Vol. {\bf 11}, (1998), pp.104-114. Pdf.
  
  
• "Discretely ordered modules as a first-order extension of the cutting planes proof system", {\em J. Symbolic Logic}, {\bf 63(4)}, (1998), pp.1582-1596.
  
  
• "Interpolation by a game", {\em Mathematical Logic Quarterly}, {\bf 44(4}, (1998), pp.450-458.
  A preliminary version appeared in the Electronic Colloquium on Computational Complexity, Report nr.: TR97-015.
  
  
• with M.~Baaz, P.~H\'{a}jek, and D.~\v{S}vejda: "Embedding logics into product logic", {\em Studia Logica}, {\bf 61}, (1998), pp.35-47.
  
  
• with M.~Chiari: "Lifting independence results in bounded arithmetic", {\em Archive for Mathematical Logic}, {\bf 38(2)}, (1999), pp.123-138.
  
  
• ``Lower bounds for a proof system with an exponential speed-up over constant-depth Frege systems and over polynomial calculus'', in: Eds. I.Pr\'{\i}vara, P. R\accent23{u}\v{z}i\v{c}ka, 22nd Inter. Symp. {\em Mathematical Foundations of Computer Science} (Bratislava, August '97), Lecture Notes in Computer Science 1295, Springer-Verlag, (1997), pp.85-90.
  
  
• ``On the degree of ideal membership proofs from uniform families of polynomials over a finite field'', Illinois J. of Mathematics, {\bf 45(1)}, (2001), pp.41-73.
  
  
• "Uniform families of polynomial equations over a finite field and structures admitting an Euler characteristic of definable sets", Proc. London Mathematical Society, {\bf 3 (81)}, (2000), pp.257-284.
  Pdf.
  
  
• "On the weak pigeonhole principle", Fundamenta Mathematicae, Vol.170(1-3), (2001), pp.123-140. Pdf.
  
  
• with T. Scanlon: "Combinatorics with definable sets: Euler characteristics and Grothendieck rings", {\em Bulletin of Symbolic Logic}, {\bf 3(3)}, (2000), pp.311-330.
  Pdf.
  
  
• "Tautologies from pseudo-random generators", Bulletin of Symbolic Logic, 7(2), (2001), pp.197-212. Pdf.
  A (shorter) preliminary version appeared in the Electronic Colloquium on Computational Complexity, Report nr.: TR00-033.
  
  
• with R. Impagliazzo: ``A note on conservativity relations among bounded arithmetic theories'', Mathematical Logic Quaterly, 48(3), (2002), pp.375-7. Pdf.
  
  
• Combinatorics of first order structures and propositional proof systems, Archive for Mathematical Logic, 43(4), (2004), pp.427-441. Pdf.
  
  
• Interpolation and approximate semantic derivations , Mathematical Logic Quaterly, Vol.48(4), (2002), pp.602-606. Pdf.
  
  
• Approximate Euler characteristic, dimension, and weak pigeonhole principles, J. of Symbolic Logic, 69(1), (2004), pp.201-214. Pdf.
  
  
• Dehn function and length of proofs , International Journal of Algebra and Computation, Vol. 13(5), (October 2003), pp.527-542.
  
  
• Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds , J. of Symbolic Logic, 69(1), (2004), pp.265-286. Pdf.
  
  
• Implicit proofs, J. of Symbolic Logic, 69(2), (2004), pp.387-397. Pdf.
  
  
• Diagonalization in proof complexity, Fundamenta Mathematicae, 182, (2004), pp.181-192. (preprint: ECCC report number TR04-018, 2004).
  
  
• Structured pigeonhole principle, search problems and hard tautologies, J. of Symbolic Logic, 70(2), (2005), pp.619-630. Pdf file.
  
  
• Substitutions into propositional tautologies, Information Processing Letters, 101, (2007), pp.163-167. Pdf file.
  
  
• with A.Skelley and N.Thapen: NP search problems in low fragments of bounded arithmetic, J. of Symbolic Logic, 72(2), (2007), pp. 649-672. Pdf file.
  
  
• with S.Cook, Consequences of the Provability of NP \subseteq P/poly, J. of Symbolic Logic, 72(4), (2007), pp. 1353-1371. Pdf file.
  
  
• An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams,
  J. of Symbolic Logic, 73(1), (2008), pp. 227-237. Pdf file.
  A preliminary version appeared in the Electronic Colloquium on Computational Complexity, Report nr.: TR07-007, (2007).
  
  
• A proof complexity generator,
  in: Logic, Methodology and Philosophy of Science: Proc. of the 13th International Congress, Eds. Clark Glymour, Wei Wang, and Dag Westerstahl, College Publications, London, (2009), pp.185-190.
  ISBN-13: 978-1-904987-45-1. Pdf file.
  
  
• A form of feasible interpolation for constant depth Frege systems ,
  J. of Symbolic Logic, 75(2), (2010), pp. 774-784. Pdf file.
  
  
• A note on propositional proof complexity of some Ramsey-type statements,
  Archive for Mathematical Logic, 50(1-2), (2011), pp.245-255. Pdf file.
  Online publication (12.Oct. 2010), DOI: 10.1007/s00153-010-0212-9.
  
  
• On the proof complexity of the Nisan-Wigderson generator based on a hard NP \cap coNP function,
  J. of Mathematical Logic, Vol.11 (1), (2011), pp.11-27.
  DOI: 10.1142/S0219061311000979
  A preliminary version appeared as ECCC report TR10-054.
  
  
• A note on SAT algorithms and proof complexity,
  Information Processing Letters, 112 (2012), pp. 490-493.
  DOI: 10.1016/j.ipl.2012.03.009
  Revised pdf and ps.
  
  
• Pseudo-finite hard instances for a student-teacher game with a Nisan-Wigderson generator,
  Logical methods in Computer Science, Vol. 8 (3:09) 2012, pp.1-8.
  DOI: 10.2168/LMCS-8(3:9)2012
  Abstr./arXiv, revised pdf and ps.
  
  
• A saturation property of structures obtained by forcing with a compact family of random variables,
  Archive for Mathematical Logic, 52(1), (2013), pp.19-28.
  Online publication (13.September 2012), DOI: 10.1007/s00153-012-0304-9
  Abstr./arXiv (preprint February 2012), revised pdf and ps.
  
  
• On the computational complexity of finding hard tautologies,
  Bulletin of the London Mathematical Society, 46(1), (2014), pp.111-125.
  Online published October 6, 2013; DOI: 10.1112/blms/bdt071
  ArXiv/abstr. (preprint December 2012).
  
  
• A reduction of proof complexity to computational complexity for $AC^0[p]$ Frege systems,
  Proceedings of the AMS, 143(11), (2015), pp.4951-4965.
  Online published 2.April 2015: DOI: 10.1090/S0002-9939-2015-12610-X .
  ArXiv/abstr, revised pdf and ps, (preprint appeared as ECCC Report TR13-156).
  
  
• Consistency of circuit evaluation, extended resolution and total NP search problems,
  Forum of Mathematics, Sigma / Volume 4 / 2016, e15: DOI: 10.1017/fms.2016.13.
  ArXiv/abstr., revised pdf and ps.
  
  
• with Igor C. Oliveira,
  Unprovability of circuit upper bounds in Cook's theory PV,
  Logical methods in Computer Science, Volume 13, Issue 1, (2017).
  DOI : 10.23638/LMCS-13(1:4)2017.
  ArXiv/abstr., revised pdf and ps. ECCC TR16-071.
  
  
• A feasible interpolation for random resolution,
  Logical Methods in Computer Science, Volume 13, Issue 1, (2017).
  DOI : 10.23638/LMCS-13(1:5)2017.
  ArXiv/abstr.. Revised pdf and ps.
  
  
• Randomized feasible interpolation and monotone circuits with a local oracle,
  J. of Mathematical Logic, Vol.18., No. 2, 1850012 (2018).
  DOI: 10.1142/S0219061318500125
  ArXiv/abstr. and pdf (preprint November 2016, revised March 2018).
  
  
• with Igor C.Oliveira,
  On monotone circuits with local oracles and clique lower bounds,
  Chicago Journal of Theoretical Computer Science, vol.2018, nb.1, (March 2018), pp.1-18.
  DOI: 10.4086/cjtcs.2018.001.
  ArXiv/abstr.
  
  
• with Jan Bydzovsky and Igor C.Oliveira,
  Consistency of circuit lower bounds with bounded theories,
  Logical Methods in Computer Science, Volume 16, Issue 2, (June 18, 2020).
  DOI:10.23638/LMCS-16(2:12)2020.
  ArXiv/abstr. and ECCC (TR19-077).
  
  
• A limitation on the KPT interpolation,
  Logical Methods in Computer Science, Vol.16, Issue 3, (August 12, 2020).
  DOI: 10.23638/LMCS-16(3:9)2020
  ArXiv/abstr, pdf.
  
  
• Small circuits and dual weak PHP in the universal theory of p-time algorithms,
  ACM Transactions on Computational Logic, 22, 2, Article 11 (May 2021).
  DOI: https://doi.org/10.1145/3446207
  (preprint April 2020, revision Dec.'20), revised pdf.
  ArXiv/abstract.
  
  
• Information in propositional proofs and algorithmic proof search,
  J. of Symbolic Logic, vol.87, nb.2, (June 2022), pp.852-869.
  DOI: https://www.doi.org/10.1017/jsl.2021.75,
  revised pdf, (preliminary version February 2021, 1st revision April 2021, 2nd revision September 2021),
  JSL "preproof" (online published 27.IX.2021), ArXiv/abstract and ECCC (TR21-053).
  
  
• On the existence of strong proof complexity generators,
  Revised pdf (preliminary version August 2022),
  ArXiv/abstract, ECCC (TR22-120) .
  
  
• Extended Nullstellensatz proof systems,
  Revised pdf (preliminary version January 2023),
  ArXiv/abstract, ECCC (TR23-007).
  
  
• A proof complexity conjecture and the Incompleteness theorem,
  Pdf (preliminary version March 2023),
  ArXiv/abstract, ECCC (TR23-030).

Lecture notes (old)

---

• Propositional proof complexity I. and some corrections.
  
  
• Proof complexity and arithmetic.

Books

---

• "Bounded arithmetic, propositional logic, and complexity theory",
  Encyclopedia of Mathematics and Its Applications, Vol.60, Cambridge University Press, Cambridge - New York - Melbourne, (1995), 343pp.
  ISBN 0-521-45205-8.
  Preface and contents, and corrections (also available from the CUP - in the resources tab at the bottom of the page).
  A version as an ebook.
  
  
• "Forcing with random variables and proof complexity",
  London Mathematical Society Lecture Note Series, No.382, Cambridge University Press, Cambridge - New York - Melbourne, (2011), 264pp.
  ISBN-13: 9780521154338.
  Corrections (also available from the CUP - in the resources tab at the bottom of the page).
  Some courses: Toronto and Vienna, and reviews (Buss's and Riis's).
  
  
• "Proof complexity",
  Encyclopedia of Mathematics and Its Appplications, Vol.170, Cambridge University Press, Cambridge - New York - Melbourne, (March 2019), 530pp.
  ISBN: 9781108416849.
  The final manuscript and corrections, typos and further remarks.

Edited volumes

---

• with P. Clote, "Arithmetic, Proof Theory and Computational Complexity",
  Oxford University Press, (1993).
  
  
• "Complexity of computations and proofs",
  Quaderni di Matematica, Vol.13, ser. published by Seconda Universita di Napoli, Caserta. 424 pp., (2004).
  
  
• with M. Baaz and S. Friedman, "Logic Colloquium'01",
  Proceedings of the European ASL meeting in Vienna 2001,
  LN in Logic, Vol.20, Assoc. for Symb. Logic, A K Peters, Ltd., and Wellesley (Mass.US), 486 pp., (2005).