COMPUTING DEFINITE LOGIC PROGRAMS BY PARTIAL INSTANTIATION

Query processing in ground definite deductive databases is known to co rrespond precisely to a linear programming problem. However, the ''gro undedness'' requirement is a huge drawback to using linear programming techniques for logic program computations because the ground version of a logic program can be very large when compared to the original log ic program. Furthermore, when we move from propositional logic program s to first-order logic programs, this effectively means that functions symbols may not occur in clauses. In this paper, we develop a theory of ''instantiate-by-need'' that performs instantiations (not necessari ly ground instantiations) only when needed. We prove that this method is sound and complete when computing answer substitutions for non-grou nd logic programs including those containing function symbols. More im portantly, when taken in conjunction with Colmerauer's result that uni fication can be viewed as linear programming, this means that resoluti on with unification can be completely replaced by linear programming a s an operational paradigm. Additionally, our tree construction method is not rigidly tied to the linear programming paradigm-we will show th at given any method M (which some implementors may prefer) that can co mpute the set of atomic logical consequences of a propositional logic program, our method can use M to compute (in a sense made precise in t he paper), the set of all (not necessarily ground) atoms that are cons equences of a first-order logic program.