Research papers
(and the
most recent),

expository papers (and the most
recent ),

old lecture notes,

books and

edited volumes.

I request that those colleagues who leave some of their papers behind pay-walls (and do not keep freely available even preliminary versions) do contribute for each download here 10 EUR to a good cause.

## 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)

## 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).