Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR13-016 | 10th April 2013 11:43

The Complexity of Theorem Proving in Autoepistemic Logic

RSS-Feed




Revision #1
Authors: Olaf Beyersdorff
Accepted on: 10th April 2013 11:43
Downloads: 2464
Keywords: 


Abstract:

Autoepistemic logic is one of the most successful formalisms for nonmonotonic reasoning. In this paper we provide a proof-theoretic analysis of sequent calculi for credulous and sceptical reasoning in propositional autoepistemic logic, introduced by Bonatti and Olivetti (ACM ToCL, 2002). 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. This contrasts with the situation in sceptical autoepistemic reasoning where we obtain an exponential lower bound to the proof length in Bonatti and Olivetti's calculus.


Paper:

TR13-016 | 17th January 2013 17:21

The Complexity of Theorem Proving in Autoepistemic Logic





TR13-016
Authors: Olaf Beyersdorff
Publication: 25th January 2013 15:42
Downloads: 2827
Keywords: 


Abstract:

Autoepistemic logic is one of the most successful formalisms for nonmonotonic reasoning. In this paper we provide a proof-theoretic analysis of sequent calculi for credulous and sceptical reasoning in propositional autoepistemic logic, introduced by Bonatti and Olivetti (ACM ToCL, 2002). 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. This contrasts with the situation in sceptical autoepistemic reasoning where we obtain an exponential lower bound to the proof length in Bonatti and Olivetti's calculus.



ISSN 1433-8092 | Imprint