default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDOlaf Beyersdorff
Person information
- affiliation: University of Jena, Germany
- affiliation (former): University of Leeds, School of Computing, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j45]Benjamin Böhm
, Tomás Peitl, Olaf Beyersdorff:
QCDCL with cube learning or pure literal elimination - What is best? Artif. Intell. 336: 104194 (2024)- [j44]Benjamin Böhm, Olaf Beyersdorff:
QCDCL vs QBF Resolution: Further Insights. J. Artif. Intell. Res. 81: 741-769 (2024) - [j43]Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff:
Should Decisions in QCDCL Follow Prefix Order? J. Autom. Reason. 68(1): 5 (2024) - [j42]Olaf Beyersdorff, Judith Clymo, Stefan S. Dantchev, Barnaby Martin:
The Riis Complexity Gap for QBF Resolution. J. Satisf. Boolean Model. Comput. 15(1): 9-25 (2024) - [j41]Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann:
Proof Complexity of Propositional Model Counting. J. Satisf. Boolean Model. Comput. 15(1): 27-59 (2024) - [j40]Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood:
Hard QBFs for Merge Resolution. ACM Trans. Comput. Theory 16(2): 6:1-6:24 (2024) - [j39]Olaf Beyersdorff, Joshua Lewis Blinkhorn, Tomás Peitl:
Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths. ACM Trans. Comput. Theory 16(4): 22:1-22:25 (2024) - [c57]Olaf Beyersdorff, Benjamin Böhm, Meena Mahajan:
Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs. AAAI 2024: 7943-7951 - [c56]Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, Luc Nicolas Spachmann:
Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree. MFCS 2024: 27:1-27:15 - [c55]Olaf Beyersdorff, Johannes Klaus Fichte, Markus Hecher, Tim Hoffmann, Kaspar Kasche:
The Relative Strength of #SAT Proof Systems. SAT 2024: 5:1-5:19 - [e2]Olaf Beyersdorff, Mamadou Moustapha Kanté, Orna Kupferman, Daniel Lokshtanov:
41st International Symposium on Theoretical Aspects of Computer Science, STACS 2024, March 12-14, 2024, Clermont-Ferrand, France. LIPIcs 289, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2024, ISBN 978-3-95977-311-9 [contents] - [i60]Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann:
Proof Complexity of Propositional Model Counting. Electron. Colloquium Comput. Complex. TR24 (2024) - [i59]Olaf Beyersdorff, Kaspar Kasche, Luc Nicolas Spachmann:
Polynomial Calculus for Quantified Boolean Logic: Lower Bounds through Circuits and Degree. Electron. Colloquium Comput. Complex. TR24 (2024) - [i58]Agnes Schleitzer, Olaf Beyersdorff:
Computationally Hard Problems Are Hard for QBF Proof Systems Too. Electron. Colloquium Comput. Complex. TR24 (2024) - 2023
- [j38]Agnes Schleitzer, Olaf Beyersdorff:
Classes of Hard Formulas for QBF Resolution. J. Artif. Intell. Res. 77: 1455-1487 (2023) - [j37]Benjamin Böhm, Olaf Beyersdorff:
Lower Bounds for QCDCL via Formula Gauge. J. Autom. Reason. 67(4): 35 (2023) - [j36]Olaf Beyersdorff, Benjamin Böhm:
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. Log. Methods Comput. Sci. 19(2) (2023) - [j35]Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl:
Hardness Characterisations and Size-width Lower Bounds for QBF Resolution. ACM Trans. Comput. Log. 24(2): 10:1-10:30 (2023) - [c54]Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann:
Proof Complexity of Propositional Model Counting. SAT 2023: 2:1-2:18 - [c53]Benjamin Böhm, Olaf Beyersdorff:
QCDCL vs QBF Resolution: Further Insights. SAT 2023: 4:1-4:17 - [i57]Benjamin Böhm, Olaf Beyersdorff:
QCDCL vs QBF Resolution: Further Insights. Electron. Colloquium Comput. Complex. TR23 (2023) - 2022
- [j34]Sarah Sigley, Olaf Beyersdorff:
Proof Complexity of Modal Resolution. J. Autom. Reason. 66(1): 1-41 (2022) - [c52]Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff:
QCDCL with Cube Learning or Pure Literal Elimination - What is Best? IJCAI 2022: 1781-1787 - [c51]Agnes Schleitzer, Olaf Beyersdorff:
Classes of Hard Formulas for QBF Resolution. SAT 2022: 5:1-5:18 - [c50]Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff:
Should Decisions in QCDCL Follow Prefix Order? SAT 2022: 11:1-11:19 - [i56]Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, Andy Oertel:
Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411). Dagstuhl Reports 12(10): 84-105 (2022) - [i55]Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff:
Should decisions in QCDCL follow prefix order? Electron. Colloquium Comput. Complex. TR22 (2022) - [i54]Agnes Schleitzer, Olaf Beyersdorff:
Classes of Hard Formulas for QBF Resolution. Electron. Colloquium Comput. Complex. TR22 (2022) - 2021
- [j33]Olaf Beyersdorff, Joshua Blinkhorn:
A simple proof of QBF hardness. Inf. Process. Lett. 168: 106093 (2021) - [j32]Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan:
Building Strategies into QBF Proofs. J. Autom. Reason. 65(1): 125-154 (2021) - [c49]Olaf Beyersdorff, Benjamin Böhm:
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. ITCS 2021: 12:1-12:20 - [c48]Olaf Beyersdorff, Luca Pulina, Martina Seidl, Ankit Shukla:
QBFFam: A Tool for Generating QBF Families from Proof Complexity. SAT 2021: 21-29 - [c47]Benjamin Böhm, Olaf Beyersdorff:
Lower Bounds for QCDCL via Formula Gauge. SAT 2021: 47-63 - [p1]Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, Martina Seidl:
Quantified Boolean Formulas. Handbook of Satisfiability 2021: 1177-1221 - [i53]Olaf Beyersdorff, Benjamin Böhm:
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. CoRR abs/2109.04862 (2021) - [i52]Olaf Beyersdorff, Benjamin Böhm:
QCDCL with Cube Learning or Pure Literal Elimination - What is best? Electron. Colloquium Comput. Complex. TR21 (2021) - [i51]Olaf Beyersdorff, Joshua Blinkhorn, Tomás Peitl:
Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths. Electron. Colloquium Comput. Complex. TR21 (2021) - 2020
- [j31]Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, Ján Pich:
Frege Systems for Quantified Boolean Logic. J. ACM 67(2): 9:1-9:36 (2020) - [j30]Olaf Beyersdorff, Joshua Blinkhorn:
Lower Bound Techniques for QBF Expansion. Theory Comput. Syst. 64(3): 400-421 (2020) - [j29]Olaf Beyersdorff, Joshua Blinkhorn:
Dynamic QBF Dependencies in Reduction and Expansion. ACM Trans. Comput. Log. 21(2): 8:1-8:27 (2020) - [j28]Olaf Beyersdorff, Luke Hinde, Ján Pich:
Reasons for Hardness in QBF Proof Systems. ACM Trans. Comput. Theory 12(2): 10:1-10:27 (2020) - [c46]Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood:
Hard QBFs for Merge Resolution. FSTTCS 2020: 12:1-12:15 - [c45]Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan:
Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution. LICS 2020: 209-223 - [c44]Olaf Beyersdorff, Joshua Blinkhorn, Tomás Peitl:
Strong (D)QBF Dependency Schemes via Tautology-Free Resolution Paths. SAT 2020: 394-411 - [i50]Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood:
Hard QBFs for Merge Resolution. CoRR abs/2012.06779 (2020) - [i49]Olaf Beyersdorff, Uwe Egly, Meena Mahajan, Cláudia Nalon:
SAT and Interactions (Dagstuhl Seminar 20061). Dagstuhl Reports 10(2): 1-18 (2020) - [i48]Olaf Beyersdorff, Benjamin Böhm:
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. Electron. Colloquium Comput. Complex. TR20 (2020) - [i47]Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan:
Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution. Electron. Colloquium Comput. Complex. TR20 (2020) - [i46]Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood:
Hard QBFs for Merge Resolution. Electron. Colloquium Comput. Complex. TR20 (2020) - [i45]Olaf Beyersdorff, Joshua Blinkhorn, Tomás Peitl:
Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths. Electron. Colloquium Comput. Complex. TR20 (2020)
2010 – 2019
- 2019
- [j27]Olaf Beyersdorff, Luke Hinde:
Characterising tree-like Frege proofs for QBF. Inf. Comput. 268 (2019) - [j26]Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate A. Schmidt, Martin Suda:
Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. J. Autom. Reason. 63(3): 597-623 (2019) - [j25]Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah:
A game characterisation of tree-like Q-Resolution size. J. Comput. Syst. Sci. 104: 82-101 (2019) - [j24]Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde:
Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs. Log. Methods Comput. Sci. 15(1) (2019) - [j23]Olaf Beyersdorff, Leroy Chew, Mikolás Janota:
New Resolution-Based QBF Calculi and Their Proof Complexity. ACM Trans. Comput. Theory 11(4): 26:1-26:42 (2019) - [c43]Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan:
Short Proofs in QBF Expansion. SAT 2019: 19-35 - [c42]Joshua Blinkhorn, Olaf Beyersdorff:
Proof Complexity of QBF Symmetry Recomputation. SAT 2019: 36-52 - [c41]Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan:
Building Strategies into QBF Proofs. STACS 2019: 14:1-14:18 - [i44]Olaf Beyersdorff, Joshua Blinkhorn:
Proof Complexity of Symmetry Learning in QBF. Electron. Colloquium Comput. Complex. TR19 (2019) - 2018
- [j22]Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla:
Understanding cutting planes for QBFs. Inf. Comput. 262: 141-161 (2018) - [j21]Judith Clymo, Olaf Beyersdorff:
Relating size and width in variants of Q-resolution. Inf. Process. Lett. 138: 1-6 (2018) - [j20]Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla:
Are Short Proofs Narrow? QBF Resolution Is Not So Simple. ACM Trans. Comput. Log. 19(1): 1:1-1:26 (2018) - [c40]Joshua Blinkhorn, Olaf Beyersdorff:
Dynamic Dependency Awareness for QBF. IJCAI 2018: 5224-5228 - [c39]Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde:
Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs. ITCS 2018: 9:1-9:18 - [c38]Olaf Beyersdorff, Joshua Blinkhorn:
Genuine Lower Bounds for QBF Expansion. STACS 2018: 12:1-12:15 - [e1]Olaf Beyersdorff, Christoph M. Wintersteiger:
Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. Lecture Notes in Computer Science 10929, Springer 2018, ISBN 978-3-319-94143-1 [contents] - [i43]Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan:
Building Strategies into QBF Proofs. Electron. Colloquium Comput. Complex. TR18 (2018) - [i42]Olaf Beyersdorff, Judith Clymo:
More on Size and Width in QBF Resolution. Electron. Colloquium Comput. Complex. TR18 (2018) - [i41]Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan:
Short Proofs in QBF Expansion. Electron. Colloquium Comput. Complex. TR18 (2018) - [i40]Olaf Beyersdorff, Judith Clymo, Stefan S. Dantchev, Barnaby Martin:
The Riis Complexity Gap for QBF Resolution. Electron. Colloquium Comput. Complex. TR18 (2018) - 2017
- [j19]Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla:
Feasible Interpolation for QBF Resolution Calculi. Log. Methods Comput. Sci. 13(2) (2017) - [c37]Olaf Beyersdorff, Luke Hinde, Ján Pich:
Reasons for Hardness in QBF Proof Systems. FSTTCS 2017: 14:1-14:15 - [c36]Joshua Blinkhorn, Olaf Beyersdorff:
Shortening QBF Proofs with Dependency Schemes. SAT 2017: 263-280 - [i39]Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde:
Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs. CoRR abs/1712.03626 (2017) - [i38]Olaf Beyersdorff, Joshua Blinkhorn:
Formulas with Large Weight: a New Technique for Genuine QBF Lower Bounds. Electron. Colloquium Comput. Complex. TR17 (2017) - [i37]Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde:
Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs. Electron. Colloquium Comput. Complex. TR17 (2017) - [i36]Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla:
Understanding Cutting Planes for QBFs. Electron. Colloquium Comput. Complex. TR17 (2017) - [i35]Olaf Beyersdorff, Luke Hinde, Ján Pich:
Reasons for Hardness in QBF Proof Systems. Electron. Colloquium Comput. Complex. TR17 (2017) - 2016
- [c35]Olaf Beyersdorff, Leroy Chew, Mikolas Janota:
Extension Variables in QBF Resolution. AAAI Workshop: Beyond NP 2016 - [c34]Olaf Beyersdorff, Joshua Blinkhorn:
Dependency Schemes in QBF Calculi: Semantics and Soundness. CP 2016: 96-112 - [c33]Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla:
Understanding Cutting Planes for QBFs. FSTTCS 2016: 40:1-40:15 - [c32]Olaf Beyersdorff, Ilario Bonacina, Leroy Chew:
Lower Bounds: From Circuits to QBF Proof Systems. ITCS 2016: 249-260 - [c31]Olaf Beyersdorff, Ján Pich:
Understanding Gentzen and Frege Systems for QBF. LICS 2016: 146-155 - [c30]Joshua Blinkhorn, Olaf Beyersdorff:
Dependency Schemes in QBF Calculi: Semantics and Soundness. QBF@SAT 2016: 41-48 - [c29]Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda:
Lifting QBF Resolution Calculi to DQBF. SAT 2016: 490-499 - [c28]Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla:
Are Short Proofs Narrow? QBF Resolution is not Simple. STACS 2016: 15:1-15:14 - [i34]Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda:
Lifting QBF Resolution Calculi to DQBF. CoRR abs/1604.08058 (2016) - [i33]Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla:
Feasible Interpolation for QBF Resolution Calculi. CoRR abs/1611.01328 (2016) - [i32]Olaf Beyersdorff, Nadia Creignou, Uwe Egly, Heribert Vollmer:
SAT and Interactions (Dagstuhl Seminar 16381). Dagstuhl Reports 6(9): 74-93 (2016) - [i31]Olaf Beyersdorff, Joshua Blinkhorn:
Dependency Schemes in QBF Calculi: Semantics and Soundness. Electron. Colloquium Comput. Complex. TR16 (2016) - [i30]Olaf Beyersdorff, Leroy Chew, Mikolas Janota:
Extension Variables in QBF Resolution. Electron. Colloquium Comput. Complex. TR16 (2016) - [i29]Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda:
Lifting QBF Resolution Calculi to DQBF. Electron. Colloquium Comput. Complex. TR16 (2016) - [i28]Olaf Beyersdorff, Ján Pich:
Understanding Gentzen and Frege systems for QBF. Electron. Colloquium Comput. Complex. TR16 (2016) - 2015
- [c27]Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla:
Feasible Interpolation for QBF Resolution Calculi. ICALP (1) 2015: 180-192 - [c26]Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah:
A Game Characterisation of Tree-like Q-resolution Size. LATA 2015: 486-498 - [c25]Olaf Beyersdorff, Leroy Chew, Mikolás Janota:
Proof Complexity of Resolution-based QBF Calculi. STACS 2015: 76-89 - [i27]Olaf Beyersdorff, Ilario Bonacina, Leroy Chew:
Lower bounds: from circuits to QBF proof systems. Electron. Colloquium Comput. Complex. TR15 (2015) - [i26]Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla:
Feasible Interpolation for QBF Resolution Calculi. Electron. Colloquium Comput. Complex. TR15 (2015) - [i25]Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla:
Are Short Proofs Narrow? QBF Resolution is not Simple. Electron. Colloquium Comput. Complex. TR15 (2015) - 2014
- [c24]Olaf Beyersdorff, Leroy Chew:
The Complexity of Theorem Proving in Circumscription and Minimal Entailment. IJCAR 2014: 403-417 - [c23]Olaf Beyersdorff, Leroy Chew, Mikolas Janota:
On Unification of QBF Resolution-Based Calculi. MFCS (2) 2014: 81-93 - [c22]Olaf Beyersdorff, Oliver Kullmann:
Unified Characterisations of Resolution Hardness Measures. SAT 2014: 170-187 - [i24]Olaf Beyersdorff, Leroy Chew:
Tableau vs. Sequent Calculi for Minimal Entailment. CoRR abs/1405.1565 (2014) - [i23]Olaf Beyersdorff, Edward A. Hirsch, Jan Krajícek, Rahul Santhanam:
Optimal algorithms and proofs (Dagstuhl Seminar 14421). Dagstuhl Reports 4(10): 51-68 (2014) - [i22]Olaf Beyersdorff, Leroy Chew:
The Complexity of Theorem Proving in Circumscription and Minimal Entailment. Electron. Colloquium Comput. Complex. TR14 (2014) - [i21]Olaf Beyersdorff, Leroy Chew:
Tableau vs. Sequent Calculi for Minimal Entailment. Electron. Colloquium Comput. Complex. TR14 (2014) - [i20]Olaf Beyersdorff, Leroy Chew, Mikolas Janota:
Proof Complexity of Resolution-based QBF Calculi. Electron. Colloquium Comput. Complex. TR14 (2014) - [i19]Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah:
A game characterisation of tree-like Q-Resolution size. Electron. Colloquium Comput. Complex. TR14 (2014) - [i18]Mikolas Janota, Leroy Chew, Olaf Beyersdorff:
On Unification of QBF Resolution-Based Calculi. Electron. Colloquium Comput. Complex. TR14 (2014) - 2013
- [j18]Olaf Beyersdorff, Nicola Galesi, Massimo Lauria:
A characterization of tree-like Resolution size. Inf. Process. Lett. 113(18): 666-671 (2013) - [j17]Olaf Beyersdorff, Nicola Galesi, Massimo Lauria:
Parameterized Complexity of DPLL Search Procedures. ACM Trans. Comput. Log. 14(3): 20:1-20:21 (2013) - [j16]Olaf Beyersdorff, Samir Datta, Andreas Krebs, Meena Mahajan, Gido Scharfenberger-Fabian, Karteek Sreenivasaiah, Michael Thomas, Heribert Vollmer:
Verifying proofs in constant depth. ACM Trans. Comput. Theory 5(1): 2:1-2:23 (2013) - [c21]Olaf Beyersdorff:
The Complexity of Theorem Proving in Autoepistemic Logic. SAT 2013: 365-376 - [i17]Olaf Beyersdorff:
The Complexity of Theorem Proving in Autoepistemic Logic. Electron. Colloquium Comput. Complex. TR13 (2013) - 2012
- [b2]Olaf Beyersdorff:
Non-classical Aspects in Proof Complexity. Cuvillier 2012, ISBN 978-3-9540403-6-0, pp. I-XI, 1-124 - [j15]Olaf Beyersdorff, Arne Meier, Michael Thomas, Heribert Vollmer:
The complexity of reasoning for fragments of default logic. J. Log. Comput. 22(3): 587-604 (2012) - [j14]Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, Alexander A. Razborov:
Parameterized Bounded-Depth Frege Is not Optimal. ACM Trans. Comput. Theory 4(3): 7:1-7:16 (2012) - [i16]Olaf Beyersdorff, Samir Datta, Andreas Krebs, Meena Mahajan, Gido Scharfenberger-Fabian, Karteek Sreenivasaiah, Michael Thomas, Heribert Vollmer:
Verifying Proofs in Constant Depth. Electron. Colloquium Comput. Complex. TR12 (2012) - [i15]Olaf Beyersdorff, Nicola Galesi, Massimo Lauria:
A Characterization of Tree-Like Resolution Size. Electron. Colloquium Comput. Complex. TR12 (2012) - 2011
- [j13]Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, Heribert Vollmer:
Proof complexity of propositional default logic. Arch. Math. Log. 50(7-8): 727-742 (2011) - [j12]