Computing Definite Logic Programs by Partial Instantiation

摘要

Query processing in ground definite deductive databases is known to correspondprecisely 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 logic 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