COMPUTING MINIMAL MODELS BY PARTIAL INSTANTIATION

Unlike sets of definite Horn clauses, logic programs with disjunctions of atoms in clause heads are often interpreted in terms of minimal mo dels. It is also well known that the minimal models of logic programs are closely related to the so-called stable models of logic programs w ith nonmonotonic negation in clause bodies, as well as to circumscript ion. Methods to compute minimal models of logic programs are becoming increasingly important as an intermediate step in the computation of s tructures associated with nonmonotonic logic programs. However, to dat e, all these techniques have been restricted to the case of propositio nal logic programs which means that an ordinary disjunctive logic prog ram must be ''grounded out'' prior to computation. Grounding out in th is manner leads to a combinatorial explosion in the number of clauses, and hence, is unacceptable. In this paper, we show how, given any met hod M which correctly computes the set of minimal models of a proposit ional logic program, we can develop a strategy to compute truth in a m inimal model of a disjunctive logic program P. The novel feature of ou r method is that it works on an ''instantiate-by-need'' basis, and thu s avoids unnecessary grounding.