| 2026 | AAAI | Proof Systems for Tensor-based Model Counting. | Olaf Beyersdorff, Joachim Giesen, Andreas Goral, Tim Hoffmann, Kaspar Kasche, Christoph Staudt |
| 2026 | AAAI | Proof Systems That Tightly Characterise Model Counting Algorithms. | Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche |
| 2026 | SAT | Proof Systems for QBF Synthesis: Extracting Skolem and Herbrand Functions. | S. Akshay, Olaf Beyersdorff, Supratik Chakraborty, Lea Kasche, Meena Mahajan, Luc Nicolas Spachmann |
| 2026 | SAT | Towards Understanding the Complexity of CAQE: A Proof-Theoretic Analysis of Its Core Procedure. | Benjamin Bhm, Olaf Beyersdorff |
| 2025 | AAAI | Computationally Hard Problems Are Hard for QBF Proof Systems Too. | Agnes Schleitzer, Olaf Beyersdorff |
| 2025 | SAT | Semi-Algebraic Proof Systems for QBF. | Olaf Beyersdorff, Ilario Bonacina, Kaspar Kasche, Meena Mahajan, Luc Nicolas Spachmann |
| 2024 | AAAI | Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs. | Olaf Beyersdorff, Benjamin Bhm, Meena Mahajan |
| 2024 | MFCS | Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree. | Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, Luc Nicolas Spachmann |
| 2024 | SAT | The Relative Strength of #SAT Proof Systems. | Olaf Beyersdorff, Johannes Klaus Fichte, Markus Hecher, Tim Hoffmann, Kaspar Kasche |
| 2023 | SAT | QCDCL vs QBF Resolution: Further Insights. | Benjamin Bhm, Olaf Beyersdorff |
| 2023 | SAT | Proof Complexity of Propositional Model Counting. | Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann |
| 2022 | IJCAI | QCDCL with Cube Learning or Pure Literal Elimination - What is Best? | Benjamin Bhm, Toms Peitl, Olaf Beyersdorff |
| 2022 | SAT | Should Decisions in QCDCL Follow Prefix Order? | Benjamin Bhm, Toms Peitl, Olaf Beyersdorff |
| 2022 | SAT | Classes of Hard Formulas for QBF Resolution. | Agnes Schleitzer, Olaf Beyersdorff |
| 2021 | SAT | QBFFam: A Tool for Generating QBF Families from Proof Complexity. | Olaf Beyersdorff, Luca Pulina, Martina Seidl, Ankit Shukla |
| 2021 | SAT | Lower Bounds for QCDCL via Formula Gauge. | Benjamin Bhm, Olaf Beyersdorff |
| 2020 | LICS | Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution. | Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan |
| 2020 | SAT | Strong (D)QBF Dependency Schemes via Tautology-Free Resolution Paths. | Olaf Beyersdorff, Joshua Blinkhorn, Toms Peitl |
| 2019 | STACS | Building Strategies into QBF Proofs. | Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan |
| 2019 | SAT | Short Proofs in QBF Expansion. | Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan |
| 2019 | SAT | Proof Complexity of QBF Symmetry Recomputation. | Joshua Blinkhorn, Olaf Beyersdorff |
| 2018 | IJCAI | Dynamic Dependency Awareness for QBF. | Joshua Blinkhorn, Olaf Beyersdorff |
| 2018 | STACS | Genuine Lower Bounds for QBF Expansion. | Olaf Beyersdorff, Joshua Blinkhorn |
| 2017 | SAT | Shortening QBF Proofs with Dependency Schemes. | Joshua Blinkhorn, Olaf Beyersdorff |
| 2016 | AAAI | Extension Variables in QBF Resolution. | Olaf Beyersdorff, Leroy Chew, Mikolas Janota |
| 2016 | CP | Dependency Schemes in QBF Calculi: Semantics and Soundness. | Olaf Beyersdorff, Joshua Blinkhorn |
| 2016 | LICS | Understanding Gentzen and Frege Systems for QBF. | Olaf Beyersdorff, Jn Pich |
| 2016 | STACS | Are Short Proofs Narrow? QBF Resolution is not Simple. | Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla |
| 2016 | SAT | Lifting QBF Resolution Calculi to DQBF. | Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda |
| 2016 | SAT | Dependency Schemes in QBF Calculi: Semantics and Soundness. | Joshua Blinkhorn, Olaf Beyersdorff |
| 2015 | ICALP | Feasible Interpolation for QBF Resolution Calculi. | Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla |
| 2015 | LATA | A Game Characterisation of Tree-like Q-resolution Size. | Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah |
| 2015 | STACS | Proof Complexity of Resolution-based QBF Calculi. | Olaf Beyersdorff, Leroy Chew, Mikols Janota |
| 2014 | CADE | The Complexity of Theorem Proving in Circumscription and Minimal Entailment. | Olaf Beyersdorff, Leroy Chew |
| 2014 | MFCS | On Unification of QBF Resolution-Based Calculi. | Olaf Beyersdorff, Leroy Chew, Mikolas Janota |
| 2014 | SAT | Unified Characterisations of Resolution Hardness Measures. | Olaf Beyersdorff, Oliver Kullmann |
| 2013 | SAT | The Complexity of Theorem Proving in Autoepistemic Logic. | Olaf Beyersdorff |
| 2011 | ICALP | Parameterized Bounded-Depth Frege Is Not Optimal. | Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, Alexander A. Razborov |
| 2011 | MFCS | Verifying Proofs in Constant Depth. | Olaf Beyersdorff, Samir Datta, Meena Mahajan, Gido Scharfenberger-Fabian, Karteek Sreenivasaiah, Michael Thomas, Heribert Vollmer |
| 2011 | SAT | Parameterized Complexity of DPLL Search Procedures. | Olaf Beyersdorff, Nicola Galesi, Massimo Lauria |
| 2010 | SAT | Proof Complexity of Propositional Default Logic. | Olaf Beyersdorff, Arne Meier, Sebastian Mller, Michael Thomas, Heribert Vollmer |
| 2010 | TAMC | Proof Complexity of Non-classical Logics. | Olaf Beyersdorff |
| 2010 | TAMC | Different Approaches to Proof Systems. | Olaf Beyersdorff, Sebastian Mller |
| 2009 | ATMOS | Edges as Nodes - a New Approach to Timetable Information . | Olaf Beyersdorff, Yevgen Nebesov |
| 2009 | CSR | Characterizing the Existence of Optimal Proof Systems and Complete Sets for Promise Classes. | Olaf Beyersdorff, Zenon Sadowski |
| 2009 | LATA | Nondeterministic Instance Complexity and Proof Systems with Advice. | Olaf Beyersdorff, Johannes Kbler, Sebastian Mller |
| 2009 | SAT | Does Advice Help to Prove Propositional Tautologies? | Olaf Beyersdorff, Sebastian Mller |
| 2009 | SAT | The Complexity of Reasoning for Fragments of Default Logic. | Olaf Beyersdorff, Arne Meier, Michael Thomas, Heribert Vollmer |
| 2009 | SYNASC | On the Existence of Complete Disjoint NP-Pairs. | Olaf Beyersdorff |
| 2009 | TIME | Model Checking CTL is Almost Always Inherently Sequential. | Olaf Beyersdorff, Arne Meier, Michael Thomas, Heribert Vollmer, Martin Mundhenk, Thomas Schneider |
| 2008 | CSL | A Tight Karp-Lipton Collapse Result in Bounded Arithmetic. | Olaf Beyersdorff, Sebastian Mller |
| 2008 | TAMC | Logical Closure Properties of Propositional Proof Systems. | Olaf Beyersdorff |
| 2006 | CSR | Tuples of Disjoint NP-Sets. | Olaf Beyersdorff |
| 2006 | TAMC | Disjoint NP-Pairs from Propositional Proof Systems. | Olaf Beyersdorff |