Computing Intersection of Autoepistemic Expansions.
Victor W. Marek, Mirosław Truszczyński · Logic Programming and Non-Monotonic Reasoning · 1991
In this paper, we consider the question of skeptical reasoning for an important nonmonotonic reasoning system — the autoepistemic logic of Moore. Autoepistemic logic is a method of reasoning which assigns to a set of formulas the collection of theories called stable expansions. A naive method to perform skeptical autoepistemic reasoning — deciding whether a given formula φ belongs to all expansions of a theory — is to compute first all expansions and then check whether φ belongs to each of them. This approach to skeptical autoepistemic reasoning is however prohibitively inefficient. The goal of this paper is to propose a different approach to computing intersection of all expansions of a theory. Our approach does not require us to compute any expansion of a theory. It reduces the question of membership in the intersection of all expansions to the question of propositional provability. More precisely, we describe a method that assigns to a modal theory I a propositional theory PI and to a modal-free formula φ another formula φ ′ in such a manner that φ is in the intersection of all expansions of I if and only if PI ⊢ φ . In general, the theory PI is much larger than the original theory I. We have found, however, several cases when it is not so and the size of the theory PI is a polynomial in the size of I. These classes of theories are closely related to logic programs and disjunctive logic programs. Consequently, we obtain methods to check whether an atom is in the intersection of all supported (or stable) models of a (disjunctive) logic program, as well as numerous complexity results.