Proof Complexity of Propositional Default Logic

Circuits, Logic, and Games

计算机科学;物理学;数学

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

Others  :  http://drops.dagstuhl.de/opus/volltexte/2010/2526/pdf/10061.BeyersdorffOlaf.Paper.2626.pdf
PID  :  44033

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

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.