Sciweavers

SAT
2010
Springer

Proof Complexity of Propositional Default Logic

13 years 7 months ago
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.
Olaf Beyersdorff, Arne Meier, Sebastian Mülle
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2010
Where SAT
Authors Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, Heribert Vollmer
Comments (0)