Previous: TR 94-07 Next: TR 94-09

Intellektik: Technical report 94-08

On the {C}ompleteness of SLDENF - Resolution

Michael Thielscher

SLDENF-resolution combines the negation-as-failure principle for logic programs involving negation, and SLDE-resolution for logic programs with an underlying equational theory. Recently, J. Shepherdson proved the soundness of this resolution principle wrt. an extended completion semantics Shepherdson 1992. In this note, we investigate the particular problems of obtaining completeness, which are caused by adding equational theories. As a concrete result we show to what extent the classical result for hierarchical and allowed non-equational programs can be generalized.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry