A rewrite mechanism for logic programs with negation

Abstract

Pure logic pro-ams can be interpreted as rewrite programs, executable with a version of the Knuth-Bendix completion procedure called linear completion. The main advantage here is in avoiding many of the loops inherent in the resolution approach: for most productive loops, linear completion yields a finite set of answers and a finite set of rewrite rules (involving just one predicate), from which all the remaining answers can be deduced. And this 'program synthesizing' aspect can be easily combined with other loop avoiding techniques using 'marked' literals and substitutions. It is thus natural to ask how much of the rewrite mechanism carries through for deducing negative information from pure programs, and more generally for any normal logic program. In this paper we show that such an extension can be built in a natural way, with ideas from the Clark completion for normal logic programs, and the domain of constrained rewriting. The correction and completeness of this extended mechanism is proved w.r.t. the 3-valued declarative semantics of Kunen for normal programs. We also point out how the semantics of a normal program can in a certain sense be 'parametrized', in terms of the 'meta-reduction' rule set of our approach.