2026-07-22T04:54:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2526 2024-03-06T11:09:09Z ddc:004 open_access

Proof Complexity of Propositional Default Logic Beyersdorff, Olaf Meier, Arne Müller, Sebastian Thomas, Michael Vollmer, Heribert Proof complexity default logic sequent calculus 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Olaf Beyersdorff and Arne Meier and Sebastian Müller and Michael Thomas and Heribert Vollmer 2010 Is Part Of Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.10061.5 urn:nbn:de:0030-drops-25261 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.5 eng https://creativecommons.org/licenses/by/4.0/legalcode