Autoepistemic Logic as a Unified Basis for Nonmonotonic Reasoning

Reference:

Ilkka Niemelä. Autoepistemic logic as a unified basis for nonmonotonic reasoning. Research Report A24, Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory, Espoo, Finland, August 1993. Doctoral dissertation.

Abstract:

Autoepistemic logic is investigated in a general setting where autoepistemic reasoning based on a given classical logic is studied. The possible sets of autoepistemic conclusions from a set of premises are defined in terms of expansions of the premises. First Moore style expansions defined by a fixed point equation are considered and a simple finitary characterization of expansions is developed. An alternative definition is proposed where autoepistemic reasoning is formalized as a sequence of introspection steps using an enumeration of sentences. The resulting enumeration-based expansions are a proper subclass of Moore style expansions. An even more tightly grounded subclass is captured by considering only L-hierarchic enumerations. Finitary characterizations of enumeration-based and L-hierarchic expansions are developed. It is shown that autoepistemic reasoning based on Moore style, enumeration-based, and L-hierarchic 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. Default logic, forms of circumscription, answer set semantics of logic programs with classical negation, nonmonotonic truth maintenance systems, and forms of abduction are shown to be special cases of autoepistemic logic based on L-hierarchic expansions. Hence, this variant of autoepistemic logic offers a promising unified basis for nonmonotonic reasoning. A decision method for autoepistemic reasoning in the general setting is developed. The method requires as a subroutine only a theorem prover for the underlying monotonic consequence relation.

Keywords:

Nonmonotonic reasoning, autoepistemic logic, computational complexity, automated theorem proving

Suggested BibTeX entry:

@techreport{HUT-TCS-A24,
    address = {Espoo, Finland},
    author = {Ilkka Niemel{\"a}},
    institution = {Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory},
    month = {August},
    note = {Doctoral dissertation},
    number = {A24},
    pages = {162},
    title = {Autoepistemic Logic as a Unified Basis for Nonmonotonic Reasoning},
    type = {Research Report},
    year = {1993},
}