On Stratified Autoepistemic Theories

Abstract

In this paper we investigate some properties of logic approach to the formalization of common sense reasoning suggested by R. Moore in [Moore, 1985]. In particular we present a class of autoepistemic theories (called stratified autoepistemic theories) and prove that theories from this class have unique stable autoepistemic expansions and hence a clear notion of theoremhood. These results are used to establish the relationship of Autoepistemic Logic with other formalizations of non-monotonic reasoning, such as negation as failure rule and circumscription. It is also shown that classical SLDNF resolution of Prolog can be used as a deductive mechanism for a rather broad class of autoepistemic theories. Key words and phrases: common sense reasoning, autoepistemic logic, negation as failure rule, non-monotonic reasoning. (Science section).