Computation of the semantics of autoepistemic belief theories

Recently, one of the authors introduced a simple and yet powerful non-monot onic knowledge representation framework, called the Autoepistemic Logic of Beliefs, AEB. Theories in AEB are called autoepistemic belief theories. Eve ry belief theory T has been shown to have the least static expansion T whic h is computed by iterating a natural monotonic belief closure operator Psi( T) starting from T. This way, the least static expansion T of any belief th eory provides its natural non-monotonic semantics which is called the stati c semantics. It is easy to see that if a belief theory T is finite then the construction of its least static expansion T stops after countably many iterations. How ever, a somewhat surprising result obtained in this paper shows that the le ast static expansion of any finite belief theory T is in fact obtained by m eans of a single iteration of the belief closure operator Psi(T) (although this requires T to be of a special form, we also show that T can be always put in this form). This result eliminates the need for multiple iterations in the computation of static semantics and allows us to replace the fixed-p oint definition of static semantics by the equivalent explicit and straight forward definition given by (T) over bar = Psi(T) (T). The second, closely related result establishes an intriguing relationship b etween static semantics T and Clark's completions comp(T) of finite belief theories. Here we use a slightly generalized version of comp(T) (see Defini tion 3.2). It shows that the static semantics T of T is obtained by augment ing T with the set beta comp(T) = {beta F: F is an element of comp(T)} thus ensuring that all formulae that belong to Clark's completion comp(T) of T are believed to be true.