Soundness and completeness of an "efficient" negation for Prolog

Abstract

The role for logic in knowledge and artificial intelligence (AI) representation and reasoning is an interesting and active area of research. In this framework, negation plays an essential role. On the other hand, Logic Programming (LP), and Prolog as its most representative programming language, has been extensively used for the implementation of logic-based systems. However, up to now we cannot find a Prolog implementation that supports an adequate negation subsystem what precludes important uses in AI applications. By adequate we mean correct and complete as well as efficiently implemented. In fact, there is no single method with this characteristic (for instance, negation as failure is incomplete, while constructive negation is hard to implement and until our work there were no running implementation of it). In previous work, we presented a novel method for incorporating negation into a Prolog compiler which takes a number of existing methods (some modified and improved by us) and uses them in a combined fashion. The method makes use of information provided by a global analysis of the source code. However, the correctness of the system was only informally sketched. In this paper, we present a general framework that can be used either to define strategies by combination of negation techniques as well as proving correctness and completeness of the resulting system. From this framework it is possible to define new strategies and, in particular, we describe the strategy that we have implemented, proving its soundness and completeness.