Computing definite logic programs by partial instantiation

Query processing in ground definite deductive is known to correspond precisely to a linear programming problem. However, the "groundedness" 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 program. Furthermore, when we move from propositional logic programs 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 necessarily ground instantiations) only when needed. We prove that this method is sound and complete when computing answer substitutions for non-ground logic programs including those containing function symbols. More importantly, when taken in conjunction with Colmerauer's result that unification can be viewed as linear programming, this means that resolution with unification can be completely replaced by linear programming as an operational paradigm. Additionally, our tree construction method is not rigidly tied to the linear programming paradigm-we will show that given any method M (which some implementors may prefer) that can compute the set of atomic logical consequences of a propositional logic program, our method can use M to compute (in a sense made precise in the paper), the set of all (not necessarily ground) atoms that are consequences of a first-order logic program.