Jan Krajicek' bibliography

Abstracts and extended abstracts - selected

---

• with P. Beame, R. Impagliazzo, T. Pitassi, P.Pudlak 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.
  
  
• with P. Beame, R. Impagliazzo, T. Pitassi and P.Pudlak: "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.
  
  
• "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.

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. Krajicek, Oxford Press, (1993), pp.1-19.
  
  
• "A fundamental problem of mathematical logic", Annals of the Kurt Godel 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.3588293,
  ArXiv/abstr. and pdf.

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. Pudlak: "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. Pdf.
  
  
• "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,
  Bull. of Symbolic Logic, Vol.30, Issue 1, (March 2024), pp.20-40.
  DOI: https://doi.org/10.1017/bsl.2023.40
  Revised pdf (preliminary version August 2022, final revision November 2023),
  Online published 22.November 2023, ArXiv/abstract, ECCC (TR22-120) .
  
  
• Extended Nullstellensatz proof systems,
  Proc. AMS, Vol.152, Nb. 11, (November 2024), pp.4881-4892.
  Article e-published on Sept. 17, 2024.
  DOI: http://dx.doi.org/10.1090/proc/12610
  Pdf (preliminary version January 2023, revised September 2023),
  ArXiv/abstract, ECCC (TR23-007).
  
  
• A proof complexity conjecture and the Incompleteness theorem,
  J. of Symbolic Logic, to appear,
  DOI:https://doi.org/10.1017/jsl.2023.69
  Pdf (preliminary version March'23, revised Sept.'23),
  JSL online (published 19.IX.2023), ArXiv/abstract, ECCC (TR23-030).

---

All papers that may be written in future will be posted only on the ArXiv.

---

Books

---

Errata pages for all books are now in one file (and possible future updates will be done only there). The errata pages for the first three books below are no longer updated.

---

• "Bounded arithmetic, propositional logic, and complexity theory",
  Encyclopedia of Mathematics and Its Applications, Vol.60, Cambridge University Press, Cambridge - New York - Melbourne, (1995), 343 pp.
  ISBN 0-521-45205-8.
  Preface and contents, and corrections.
  
  
• "Forcing with random variables and proof complexity",
  London Mathematical Society Lecture Note Series, No.382, Cambridge University Press, Cambridge - New York - Melbourne, (2011), 264 pp.
  ISBN-13: 9780521154338.
  Corrections. Some courses: Toronto and Vienna, and reviews: S.Buss's and S.Riis's.
  Student seminar about the topic with various material available and some additional examples .
  
  
• "Proof complexity",
  Encyclopedia of Mathematics and Its Appplications, Vol.170, Cambridge University Press, Cambridge - New York - Melbourne, (2019), 530 pp.
  ISBN: 9781108416849.
  Corrections, typos and further remarks and reviews: M.Mueller's and P.Smith's (and some are at the CUP site).
  
  
• "Proof complexity generators",
  London Mathematical Society Lecture Notes Series, Vol.497, Cambridge University Press, Cambridge - New York - Melbourne, to appear in 2025, 143 pp.
  ISBN: 9781009611701.
  Final manuscript (August 2024).

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