Proof Complexity of Propositional Default Logic

Authors Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, Heribert Vollmer



PDF
Thumbnail PDF

File

DagSemProc.10061.5.pdf
  • Filesize: 450 kB
  • 14 pages

Document Identifiers

Author Details

Olaf Beyersdorff
Arne Meier
Sebastian Müller
Michael Thomas
Heribert Vollmer

Cite AsGet BibTex

Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, and Heribert Vollmer. Proof Complexity of Propositional Default Logic. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
https://doi.org/10.4230/DagSemProc.10061.5

Abstract

Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen's system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti's enhanced calculus for skeptical default reasoning.
Keywords
  • Proof complexity
  • default logic
  • sequent calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail