Autoepistemic Logic as a Unified Basis for Nonmonotonic Reasoning

摘要

Autoepistemic logic is investigated in a general setting where autoepistemicreasoning 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-heirarchic enumerations. Finitary characterizations of enumeration-based and L-heirarchic 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. 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.