Since first order logic and, especially, Horn logic is used as a programming language, the most common interpretation method for such programs is resolution. Algebraic completion and term rewriting techniques were recently proposed as an alternative to resolution oriented theorem provers. In this paper, the relation between resolution and algebraic completion (restricted to Horn logic) is closely analysed. It is shown, that both methods are equivalent in terms of inference steps and unifications, and, that using the completion method for interpreting (Horn) logic programs, no efficiency can be gained as compared with resolution.
This work has been done within a joint project of the GMD and the SFB 314 (artificial intelligence) at the University of Karlsruhe