Knuth-Bendix completion of horn clause programs for restricted linear resolution and paramodulation

Abstract

The aim of Knuth-Bendix completion is to transform an input specification into another, equivalent specification such that a given set of inference rules becomes complete for the transformed specification. In the classical case, the specifications consist of unconditional equations, and the inference rule is term rewriting. Here we investigate Knuth-Bendix completion methods for full Horn clause specifications and introduce a class of inference systems defined by an abstract concept of restrictions imposed on linear resolution and paramodulation. The usual technical ingredients of Knuth-Bendix completion methods, e.g. critical pairs, a corresponding critical pair lemma, simplification and elimination methods and critical pair criteria are generalized with respect to the concept of restrictions. We show that for any concrete restriction, our completion methods produce specifications for which linear resolution and paramodulation under the given restriction are refutationally complete. Conventional completion methods are instances of completion with respect to restrictions.