Lehr- und Forschungseinheit für Theoretische Informatik,
Institut für Informatik der Ludwig-Maximilians-Universität München

Jan Johannsen's Publications

Books, Journal Articles, Conference Articles, Reviews, Other Publications.

Submitted Articles

  1. Jan Johannsen. Backdoors into Two Occurrences . Submitted for publication, 2016.


  1. Arnold Beckmann and Jan Johannsen. Bounded Arithmetic and Resolution-Based Proof Systems. Collegium Logicum Volume 7, KGS Vienna, 2004. ISBN 3-901546-02-2.

Journal Articles

  1. Samuel R. Buss and Jan Johannsen. On Linear Resolution. Journal on Satisfiability, Boolean Modeling and Computation, accepted for publication, 2017.
  2. Maria Luisa Bonet, Samuel R. Buss and Jan Johannsen. Improved Separations of Regular Resolution from Clause Learning Proof Systems. Journal of Artificial Intelligence Research 49, pp. 669-703, 2014.
  3. Samuel R. Buss, Jan Hoffmann and Jan Johannsen. Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL-Algorithms with Clause Learning. Logical Methods in Computer Science 4 (4:13), 2008.
  4. Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, and Alasdair Urquhart. An exponential separation between regular and general resolution. Theory of Computing 3 article 5, pp. 81-102, 2007.
  5. Jan Johannsen.The complexity of pure literal elimination. Journal of Automated Reasoning 35 No. 1-3, special issue on SAT 2005, pp. 88-95, 2005.
  6. Arnold Beckmann and Jan Johannsen. An unexpected separation result in linearly bounded arithmetic. Mathematical Logic Quarterly 51 no. 2 pp. 191--200, 2005.
  7. Klaus Aehlig and Jan Johannsen. An elementary fragment of second-order lambda calculus. ACM Transactions on Computational Logic 6 no. 2, 2005. Preliminary version available on CoRR as cs.LO/0210022.
  8. Jan Johannsen. Depth lower bounds for monotone semi-unbounded fan-in circuits. RAIRO Theoretical Informatics and Applications 35 no. 3 pp. 277--286, 2001.
  9. Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen. On the relative complexity of resolution refinements and cutting planes proof systems. SIAM Journal on Computing 30 pp. 1462-1484, 2000.
  10. J. Wolfgang Degen and Jan Johannsen. Cumulative higher-order logic as a foundation for set theory. Mathematical Logic Quarterly 46 pp. 147--170, 2000.
  11. Jan Johannsen. Lower bounds for monotone real circuit depth and formula size and tree-like cutting planes. Information Processing Letters 67 pp. 37--41, 1998.
  12. Jan Johannsen. A remark on independence results for sharply bounded arithmetic. Mathematical Logic Quarterly 44 no. 4 pp. 569--570, 1998.
  13. Jan Johannsen. A model-theoretic property of sharply bounded formulae, with some applications. Mathematical Logic Quarterly 44 no. 2 pp. 205--215, 1998.
  14. Jan Johannsen. A note on sharply bounded arithmetic. Archive for Mathematical Logic 33 pp. 159--165, 1994.

Conference Articles

  1. Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard, Jakob Nordström and Marc Vinyals. Trade-Offs between Time and Memory in a Tighter Model of CDCL SAT Solvers , in: Nadia Creignou and Daniel LeBerre (eds.), Theory and Applications of Satisfiability Testing, 19th International Conference SAT 2016, Springer LNCS 9710, 2016 (to appear).
  2. Jan Johannsen. Exponential separations in a hierarchy of clause learning proof systems, in: Matti Järvisalo and Allen van Gelder (eds.), Theory and Applications of Satisfiability Testing, 16th International Conference SAT 2013, Springer LNCS 7962, pp. 40-51, 2013.
  3. Eli Ben-Sasson and Jan Johannsen. Lower Bounds for width-restricted clause learning on formulas of small width, in: Toby Walsh (ed.), Proceedings of the 22nd International Joint Conference on Artificial Intelligence, IJCAI 2011 Best paper track, pp. 2570-2575, 2011.
  4. Eli Ben-Sasson and Jan Johannsen. Lower Bounds for width-restricted clause learning on small width formulas, in: Ofer Strichman and Stefan Szeider (eds.), Theory and Applications of Satisfiability Testing, 13th International Conference SAT 2010, Springer LNCS 6175, pp. 16-29, 2010.
  5. Jan Johannsen. An exponential lower bound for width-restricted clause learning, in: Oliver Kullmann (ed.), Theory and Applications of Satisfiability Testing, 12th International Conference SAT 2009, Springer LNCS 5584, pp. 128-140, 2009.
  6. Hermann Gruber and Jan Johannsen. Optimal lower bounds on regular expression size using communication complexity, in: Roberto Amadio (ed.): Foundations of Software Science and Computational Structures, 11th Intl. Conference FOSSACS 2008, Springer LNCS 4962, pp. 273-286, 2008.
  7. Markus Jehle, Jan Johannsen, Martin Lange and Nicolas Rachinsky. Bounded model checking for all regular properties, Proceedings of the third International Workshop on Bounded Model Checking (BMC 2005), Electronic Notes in Theoretical Computer Science 144 no. 1, pp. 1-92.
  8. Jan Johannsen. Satisfiability problems complete for deterministic logarithmic space. In: Volker Diekert and Michel Habib (eds.): STACS 2004, 21st Annual Symposium on Theoretical Aspects of Computer Science, Proceedings. Springer LNCS 2996, pp. 317-325, 2004.
  9. Jan Johannsen and Martin Lange. CTL+ is complete for double exponential time. In: J. C. M. Baeten et al., editors, Proc. 30th Int. Coll. on Automata, Logics and Programming (ICALP'03), Springer LNCS 2719, pp. 767-775, 2003.
  10. Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, and Alasdair Urquhart. An exponential separation between regular and general resolution. In Proceedings of the 34th ACM Symposium on Theory of Computing (STOC), pages 448--456, 2002.
  11. Jan Johannsen and N. S. Narayanaswamy. An optimal lower bound for resolution with 2-conjunctions. In Krzysztof Diks and Wojciech Rytter, editors, Mathematical Foundations of Computer Science 2002, Springer LNCS 2420, pages 387--398, 2002.
  12. Klaus Aehlig, Jan Johannsen, Helmut Schwichtenberg, and Sebastiaan A. Terwijn. Linear ramified higher type recursion and parallel complexity. In Reinhard Kahle, Peter Schröder-Heister, and Robert Stärk, editors, Proof Theory in Computer Science, pages 1--21. Springer LNCS 2183, 2001.
  13. Jan Johannsen and Chris Pollett. On the Δb1-bit-comprehension rule. In Sam Buss, Petr Hájek, and Pavel Pudlák, editors, Logic Colloquium 98, pages 262--279. ASL Lecture Notes in Logic, 2000.
  14. Jan Johannsen. Weak bounded arithmetic, the Diffie-Hellman problem, and Constable's class K. In Proc. 14th IEEE Symposium on Logic in Computer Science, pages 268--274, 1999.
  15. Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen. Exponential separations between restricted resolution and cutting planes proof systems. In Proc. 39th Symposium on Foundations of Computer Science, pages 638--647, 1998.
  16. Jan Johannsen. Equational calculi and constant-depth propositional proofs. In Paul Beame and Samuel R. Buss, editors, Proof Complexity and Feasible Arithmetics, pages 149--162. AMS DIMACS Series Vol. 39, 1998.
  17. Jan Johannsen and Chris Pollett. On proofs about threshold circuits and counting hierarchies (extended abstract). In Proc. 13th IEEE Symposium on Logic in Computer Science, pages 444--452, 1998.
  18. Jan Johannsen. A bounded arithmetic theory for constant depth threshold circuits. In Petr Hájek, editor, GÖDEL `96, pages 224--234, 1996. Springer Lecture Notes in Logic 6.
  19. Jan Johannsen. On sharply bounded length induction. In Hans Kleine Büning, editor, Computer Science Logic, pages 362--367. Springer, 1996.
  20. Jan Johannsen. On the weakness of sharply bounded polynomial induction. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Computational Logic and Proof Theory, pages 223--230. Springer LNCS 713, 1993.


  1. Review of Ryan Williams: Faster Decision of First-Order Graph Properties. Mathematical Reviews MR3397701.
  2. Review of Olaf Beyersdorff, Leroy Chew and Karteek Sreenivasaiah: A Game Characterisation of Tree-like Q-Resolution Size. Mathematical Reviews MR3344826.
  3. Review of Yijia Chen and Jörg Flum: On Optimal Inverters. Mathematical Reviews MR3230822.
  4. Review of Arnold Beckmann and Samuel R. Buss: Characterising Definable Search problems in Bounded Arithmetic via Proof Notations. Mathematical Reviews MR2867558.
  5. Review of Alasdair Urquhart: A near-optimal separation of regular and general resolution. Mathematical Reviews MR2783204 (2012j:03137).
  6. Review of Emil Jerábek: A sorting network in bounded arithmetic. Mathematical Reviews MR2747053 (2012e:03134).
  7. Review of Emil Jerábek: On theories of bounded arithmetic for NC1. Mathematical Reviews MR2747052 (2012e:03133).
  8. Review of Nicola Galesi and Massimo Lauria: On the automatizability of Polynomial Calculus. Mathematical Reviews MR2652027 (2011k:68044).
  9. Review of Leszek Kolodziejczyk and Neil Thapen: The polynomial and linear hierarchies in V0. Mathematical Reviews MR2568761 (2011h:03125).
  10. Review of Eli Ben-Sasson: Size-space tradeoffs for resolution. Mathematical Reviews MR2506301 (2011a:68035).
  11. Review of Olaf Beyersdorff: On the correspondence between arithmetic theories and propositional proof systems - a survey. Mathematical Reviews MR2510275 (2010j:03068).
  12. Review of A. Cordón-Franco, A. Fernández-Margarit and F. F. Lara-Martín: Existentially closed models and conservation results in bounded arithmetic. Mathematical Reviews MR2475644 (2010e:03072).
  13. Review of Leszek Kolodziejczyk and Neil Thapen: The polynomial and linear hierarchies in models where the weak pigeonhole principle fails. Mathematical Reviews MR2414466 (2009g:03092).
  14. Review of Grzegorz Herman, Tim Paterson and Michael Soltys: A propositional proof system with quantification over permutations. Mathematical Reviews MR2346238 (2008m:03121).
  15. Review of Joost J. Joosten: Propositional proof systems and fast consistency provers. Mathematical Reviews MR2336354 (2008k:03065).
  16. Review of Jan Krajícek, Alan Skelley and Neil Thapen: NP search problems in low fragments of bounded arithmetic. Mathematical Reviews MR2320295 (2008i:03068).
  17. Review of Satoru Kuroda: Generalized quantifier and a bounded arithmetic theory for LOGCFL. Mathematical Reviews MR2321590 (2008e:03102).
  18. Review of Emil Jerábek: The strength of sharply bounded induction. Mathematical Reviews MR2282404 (2007k:03160).
  19. Review of Arnold Beckmann: Generalised Dynamic Ordinals - universal measures for implicit computational complexity. Mathematical Reviews MR2258702 (2007k:03160).
  20. Review of Michael Soltys: LA, permutations, and the Hajós Calculus. Mathematical Reviews MR2181385 (2006h:03053)
  21. Review of Arnold Beckmann: Uniform proof complexity. Mathematical Reviews MR2157726 (2006d:03102)

Other Publications

  1. Jan Johannsen. Schwache Fragmente der Arithmetik und Schwellwertschaltkreise beschränkter Tiefe. PhD thesis, Universität Erlangen-Nürnberg, 1996.
  2. Jan Johannsen. Semantische Vollständigkeit halbformaler Systeme der transfiniten Typentheorie. Diploma Thesis, Universität Erlangen-Nürnberg, 1991.
  3. Jan Johannsen. Kumulative Typenlogik mit einer infinitären Schlußregel. Student project, Universität Erlangen-Nüurnberg, 1990.

Home Page          TCS          Computer Science Institute          University