ABSTRACT
However, it is not enough to have some sound and complete set of rules of inference and some procedure to apply them systematically to have a logic programming system. To be satisfactory as a computation device, a proof procedure should not leave proof possibilities unchecked (search completeness), that is, the procedure should terminate without a proof only if no proof exists. We do not want our programs to terminate with no answer if there is one (except possibly for running out of computational resources such as computer memory). Furthermore, a set of premises has many consequences that are definitely irrelevant to the proof of a given consequence. The proof procedure should be goal directed in that derivations of irrelevant consequences are avoided. We do not want the computations of a program to include subcomputations that do not at least potentially contribute in some way to the program's output.
