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 [5]. 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. © 2013 Springer-Verlag.
CITATION STYLE
Beyersdorff, O. (2013). The complexity of theorem proving in autoepistemic logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7962 LNCS, pp. 365–376). https://doi.org/10.1007/978-3-642-39071-5_27
Mendeley helps you to discover research relevant for your work.