License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.10061.5
URN: urn:nbn:de:0030-drops-25261
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2526/
Go to the corresponding Portal

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

Proof Complexity of Propositional Default Logic

pdf-format:
10061.BeyersdorffOlaf.Paper.2626.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{beyersdorff_et_al:DagSemProc.10061.5,
  author =	{Beyersdorff, Olaf and Meier, Arne and M\"{u}ller, Sebastian and Thomas, Michael and Vollmer, Heribert},
  title =	{{Proof Complexity of Propositional Default Logic}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--14},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2010/2526},
  URN =		{urn:nbn:de:0030-drops-25261},
  doi =		{10.4230/DagSemProc.10061.5},
  annote =	{Keywords: Proof complexity, default logic, sequent calculus}
}

Keywords: Proof complexity, default logic, sequent calculus
Collection: 10061 - Circuits, Logic, and Games
Issue Date: 2010
Date of publication: 26.04.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI