On the Decidability and Complexity of Autoepistemic Reasoning¹

Article type: Research Article

Authors: Niemelä, Ilkka N.F.

Affiliations: Department of Computer Science, Helsinki University of Technology, Otakaari 1, SF-02150 Espoo, Finland

Note: [1] This paper is a comprehensive survey and generalization of earlier work presented at different conferences [29, 31, 32, 33, 34] containing also new results.

Abstract: The decidability and computational complexity of autoepistemic reasoning is investigated in a general setting where the autoepistemic logic CLae built on top of a given classical logic CL is studied. Correct autoepistemic conclusions from a set of premises are defined in terms of expansions of the premises. Three classes of expansions are studied: Moore style stable expansions, enumeration based expansions, and L-hierarchic expansions. A simple finitary characterization for each type of expansions in CLae is developed. Using the characterizations conditions ensuring that a set of premises has at least one or exactly one stable expansion can be stated and an upper bound for the number of stable expansions of a set of premises can be given. With the aid of the finitary characterizations results on decidability and complexity of autoepistemic reasoning are obtained. E.g., it is shown that autoepistemic reasoning based on each of the three types of expansions is decidable if the monotonic consequence relation given by the underlying classical logic is decidable. In the propositional case decision problems related to the three classes of expansions are shown to be complete problems with respect to the second level of the polynomial time hierarchy. This implies that propositional autoepistemic reasoning is strictly harder than classical propositional reasoning unless the polynomial time hierarchy collapses.

DOI: 10.3233/FI-1992-171-208

Journal: Fundamenta Informaticae, vol. 17, no. 1-2, pp. 117-155, 1992