Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Beyersdorff, Olaf; Meier, Arne; Müller, Sebastian; Thomas, Michael; Vollmer, Heribert License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-25261

; ; ; ;

Proof Complexity of Propositional Default Logic



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

  author =	{Olaf Beyersdorff and Arne Meier and Sebastian M{\"u}ller and Michael Thomas and Heribert Vollmer},
  title =	{Proof Complexity of Propositional Default Logic},
  booktitle =	{Circuits, Logic, and Games},
  year =	{2010},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th{\'e}rien and Heribert Vollmer},
  number =	{10061},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{},
  annote =	{Keywords: Proof complexity, default logic, sequent calculus}

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

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