[Back]

T. Eiter, V. Klotz, H. Tompits, S. Woltran:
"Modal Nonmonotonic Logics Revisited: Efficient Encodings for the Basic Reasoning Tasks";
Talk: Analytic Tableaux and Related Methods (TABLEAUX), Copenhagen, Denmark; 07-30-2002 - 08-01-2002; in: "Proceedings of the Eleventh Conference on Automated Reasoning with Analytic Tableaux and Related Methods", U. Egly, C. Fermüller (ed.); Springer Verlag, (2002), ISBN: 3-540-43929-3; 100 - 114.

Modal nonmonotonic logics constitute a well-known family of knowledge-representation formalisms capturing ideally rational agents
reasoning about their own beliefs. Although these formalisms are extensively studied from a theoretical point of view, most of these
approaches lack generally available solvers thus far. In this paper, we show how variants of Moore's autoepistemic logic can be axiomatised by means of quantified Boolean formulas (QBFs). More specifically, we provide polynomial reductions of the basic reasoning tasks associated
with these logics into the evaluation problem of QBFs. Since there are now efficient QBF-solvers, this reduction technique yields a practicably relevant approach to build prototype reasoning systems for these formalisms. We incorporated our encodings within the system QUIP and tested their performance on a class of benchmark problems using different underlying QBF-solvers.

http://www.kr.tuwien.ac.at/staff/stefan/tableaux02.ps.gz