Negation as Failure (NAF) as a nonmonotonic reasoning mechanism has become a central feature of advanced deductive systems. Monotonic deductive systems are not able to express severa! important queries such as those involving the set difference operator of relational systems. On the other hand, Horn clause sys­ tems extended with NAF provide a useful compromise between expressiveness and efficiency. Introduced in PLANNER [Hew72] and Prolog [Rou75], NAF has been an essential feature in the design of programming languages, databases [Ull89, GM92), truth maintenance systems (TMS) [Doy79, DK86], and many other applications. NAF allows a logic system to infer the negation of any positive atom for which the system unsuccessfully finishes attempting its proof. Infor­ mally, only justified conclusions should be accepted as valid. Formally, this notion of justification corresponds to that of logical support.