Implementing Constructive Intensional Negation

摘要

Although negation is an active area of research in logic pro-rngramming, sound and complete implementations are still absent from actual Prolog systems. One of the most promising techniques in the literature is intensional negation (IN), which follows a transformational approach: for each predicate p in a program its negative counterpart intneg(p) is generated. However, implementations of IN have not been included in Prolog environments due, in part, to the lack of details and explicit techniques, such as the treatment of universally quantified goals. In this paper, we describe a variant of IN, which we have called constructive intensional negation (CIN). Unlike earlier proposals, CIN does not resort to a dedicated resolution strategy when dealing with universally quantified formulae, which has been instrumental in having an effective implementation. Therefore, pure SLD resolution is used, what enables the reuse of existing Prolog implementation technology. Among the contributions of this work we can mention not only a full implementation being tested for its integration in the Ciao Prolog system but also some formal results ensuring soundness and completeness with their associated proofs.