Jan Krajicek' bibliography

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,
  in: "Logic, Automata, and Computational Complexity: The Works of Stephen A. Cook",
  ed.Bruce M.Kapron, Association for Computing Machinery Books, New York, NY, USA, 43, pp.83-94, May 2023.
  book DOI: 10.1145/3588287, ISBN: 979-8-4007-0779-7.
  chapter DOI: 10.1145/3588287.3588,
  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).