05977561

j

05977561 Beyersdorff, Olaf Meier, Arne M\"uller, Sebastian Thomas, Michael Vollmer, Heribert Proof complexity of propositional default logic. Arch. Math. Logic 50, No. 7-8, 727-742 (2011). 2011 Springer-Verlag, Berlin EN default logic sequent calculus proof complexity

doi:10.1007/s00153-011-0245-8

Summary: 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.