Logic programs, well-orderings, and forward chaining

We investigate the construction of stable models of general propositional logic programs. We show that a forward-chaining technique, supplemented by a properly chosen safeguard can be used to construct stable models of logic programs. Moreover, the proposed method has the advantage that if a program has no stable model, the result of the construction is a stable model of a subprogram. Further, in such a case the proposed method "isolates the inconsistency" of the program, that is it points to the part of the program responsible for the inconsistency. The results of computations are called stable submodels. We prove that every stable model of a program is a stable submodel. We investigate the complexity issues associated with stable submodels. The number of steps required to construct a stable submodel is polynomial in the sum of the lengths of the rules of the program. in the infinite case the outputs of the forward chaining procedure have much simpler complexity than those for general stable models. We show how to incorporate other techniques for finding models (e.g. Fitting operator, Van Gerder-Ross-Schlipf operator) into our construction. (C) 1999 Elsevier Science B.V. All rights reserved.