On the Weakness of Sharply Bounded Polynomial Induction. - Jan Johannsen (Kurt Gödel Colloquium, 1993)

A note on sharply bounded arithmetic. - Jan Johannsen (Arch. Math. Log., 1994)

On Sharply Bounded Length Induction. - Jan Johannsen (CSL, 1995)

Equational calculi and constant depth propositional proofs. - Jan Johannsen (Proof Complexity and Feasible Arithmetics, 1996)

Schwache Fragmente der Arithmetik und Schwellwertschaltkreise beschränkter Tiefe. - Jan Johannsen (1996)

On Proofs about Threshold Circuits and Counting Hierarchies. - Jan Johannsen; Chris Pollett (LICS, 1998)

Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems - Maria Luisa Bonet; Juan Luis Esteban; Nicola Galesi; Jan Johannsen (Electron. Colloquium Comput. Complex., 1998)

Lower Bounds for Monotone Real Circuit Depth and Formula Size and Tree-Like Cutting Planes. - Jan Johannsen (Inf. Process. Lett., 1998)

A Model Theoretic Property of Sharply Bounded Formulae, with some Applications. - Jan Johannsen (Math. Log. Q., 1998)

A Remark on Independence Results for Sharply Bounded Arithmetic. - Jan Johannsen (Math. Log. Q., 1998)

Weak Bounded Arithmetic, the Diffie-Hellman Problem and Constable's Class K. - Jan Johannsen (LICS, 1999)

Cumulative Higher-Order Logic as a Foundation for Set Theory. - Wolfgang Degen; Jan Johannsen (Math. Log. Q., 2000)

On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems. - Maria Luisa Bonet; Juan Luis Esteban; Nicola Galesi; Jan Johannsen (SIAM J. Comput., 2000)

Linear Ramified Higher Type Recursion and Parallel Complexity. - Klaus Aehlig; Jan Johannsen; Helmut Schwichtenberg; Sebastiaan Terwijn (Proof Theory in Computer Science, 2001)

An Exponential Separation between Regular and General Resolution - Michael Alekhnovich; Jan Johannsen; Toniann Pitassi; Alasdair Urquhart (Electron. Colloquium Comput. Complex., 2001)

Depth Lower Bounds for Monotone Semi-Unbounded Fan-in Circuits. - Jan Johannsen (RAIRO Theor. Informatics Appl., 2001)

An Optimal Lower Bound for Resolution with 2-Conjunctions. - Jan Johannsen; N. S. Narayanaswamy (MFCS, 2002)

CTL+ Is Complete for Double Exponential Time. - Jan Johannsen; Martin Lange (ICALP, 2003)

Satisfiability Problems Complete for Deterministic Logarithmic Space. - Jan Johannsen (STACS, 2004)

Bounded Model Checking for All Regular Properties. - Markus Jehle; Jan Johannsen; Martin Lange; Nicolas Rachinsky (BMC@CAV, 2005)

The Complexity of Pure Literal Elimination. - Jan Johannsen (J. Autom. Reason., 2005)

An unexpected separation result in Linearly Bounded Arithmetic. - Arnold Beckmann; Jan Johannsen (Math. Log. Q., 2005)

An elementary fragment of second-order lambda calculus. - Klaus Aehlig; Jan Johannsen (ACM Trans. Comput. Log., 2005)

Optimal Lower Bounds on Regular Expression Size Using Communication Complexity. - Hermann Gruber; Jan Johannsen (FoSSaCS, 2008)

Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning. - Samuel R. Buss; Jan Hoffmann 002; Jan Johannsen (Log. Methods Comput. Sci., 2008)

An Exponential Lower Bound for Width-Restricted Clause Learning. - Jan Johannsen (SAT, 2009)

Lower bounds for width-restricted clause learning on small width formulas. - Eli Ben-Sasson; Jan Johannsen (Electron. Colloquium Comput. Complex., 2010)

Lower Bounds for Width-Restricted Clause Learning on Formulas of Small Width. - Eli Ben-Sasson; Jan Johannsen (IJCAI, 2011)

Exponential Separations in a Hierarchy of Clause Learning Proof Systems. - Jan Johannsen (Electron. Colloquium Comput. Complex., 2013)

Improved Separations of Regular Resolution from Clause Learning Proof Systems. - Maria Luisa Bonet; Sam Buss; Jan Johannsen (J. Artif. Intell. Res., 2014)

Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers. - Jan Elffers; Jan Johannsen; Massimo Lauria; Thomas Magnard; Jakob Nordström; Marc Vinyals (SAT, 2016)

On Linear Resolution. - Sam Buss; Jan Johannsen (J. Satisf. Boolean Model. Comput., 2016)

Simplified and Improved Separations Between Regular and General Resolution by Lifting. - Marc Vinyals; Jan Elffers; Jan Johannsen; Jakob Nordström (SAT, 2020)

Backdoors into Two Occurrences. - Jan Johannsen (J. Satisf. Boolean Model. Comput., 2020)