A CONTEXT FOR BELIEF REVISION - FORWARD CHAINING NORMAL NONMONOTONIC RULE SYSTEMS

A number of nonmonotonic reasoning formalisms have been introduced to model the set of beliefs of an agent. These include the extensions of a default logic, the stable models of a general logic program, and the extensions of a truth maintenance system among others. In [13] and [1 6], the authors introduced nonmonotonic rule systems as a nonlogical g eneralization of all essential features of such formalisms so that the orems applying to all could be proven once and for all. In this paper, we extend Rieter's normal default theories, which have a number of th e nice properties which make them a desirable context for belief revis ion, to the setting of nonmonotonic rule systems. Reiter defined a def ault theory to be normal if all the rules of the default theory satisf ied a simple syntatic condition. However, this simple syntatic conditi on has no obvious analogue in the setting of nonmonotonic rule systems . Nevertheless, an analysis of the proofs of the main results on norma l default theories reveals that the proofs do not rely on the particul ar syntactic form of the rules but rather on the fact that all rules h ave a certain consistency property. This led us to extend the notion o f normal default theories with respect to a general consistency proper ty. This extended notion of normal default theories, which we call For ward Chaining normal (FC-normal), is easily lifted to nonmonotonic rul e systems and hence applies to general logic programs and truth mainte nance systems as well. We prove that FC-normal nonmonotonic rule syste ms have all the desirable properties possessed by normal default theor ies and a number of other important properties as well. We also give a n analysis of the complexity of the set of extensions of FC-normal non monotonic rule systems. For example, we prove that every recursive FC- normal nonomonotonic rule system has an extension which is r.e. in the halting set. Similarly any finite FC-normal nonomonotonic rule system S has an extension which can be computed in polynomial time in the si ze of S. Again these results automatically apply to general logic prog rams, truth maintenance systems, and default theories. Moreover, even in the case of normal default theories, our complexity results are new .