Title
Proof Complexity of Propositional Default Logic
Abstract
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.
Year
DOI
Venue
2010
10.1007/s00153-011-0245-8
Archive for Mathematical Logic
Keywords
Field
DocType
Default logic, Sequent calculus, Proof complexity, 03F20, 03B60
Default logic,Discrete mathematics,Natural deduction,Structural proof theory,Sequent calculus,Deductive reasoning,Sequent,Proof complexity,Cut-elimination theorem,Mathematics
Conference
Volume
Issue
ISSN
50
7-8
1432-0665
ISBN
Citations 
PageRank 
3-642-14185-4
5
0.43
References 
Authors
19
5
Name
Order
Citations
PageRank
Olaf Beyersdorff122330.33
Arne Meier212619.00
Sebastian Müller36313.40
Michael Thomas4323.22
Heribert Vollmer580571.64