A rewrite mechanism for logic programs with negation

AbstractIn several familiar cases of logic programs and queries with infinitely many answers, the usual operational mechanisms based on SLD-resolution and its extensions go into an infinite loop. It may therefore be desirable to look for mechanisms which synthesize possible structural relations on sets of answers. One such mechanism is known for pure logic programs: interpret them as rewrite programs, and execute them with a version of the Knuth-Bendix algorithm, called linear completion. W.r.t. positive queries for such programs, in most cases of productive loops, linear completion yields a finite set of answers and a finite set of rewrite rules involving just one predicate, from which the remaining answers can be deduced. It is thus natural to ask how much of the rewrite mechanism carries through for deducing negative information from pure programs, and more generally from normal logic programs. In this paper, we show that such an extension can be built in a natural way, with ideas from the Clark completion, and the domain of constrained rewriting. The correctness and completeness of this extended mechanism are proved w.r.t. the 3-valued declarative semantics of Künen for normal programs. Due to the synthesizing property and the acceptance of non ground negatives queries, our mechanism is in a sense constructive w.r.t. negation. An interesting side-effect of our approach seems to be its ability to parametrize the semantics of a normal program in terms of a meta-reduction rule set: in particular, we can operationally go beyond Künen's semantics, if desired