Duality in Logic Programming

Various approximations of classic negation have been proposed for logic programming. But the semantics for those approximations are not entirely clear. In this paper a proof-theoretic operator, we call it failure operator, denoted as FP, is associated with each logic program to characterize the meaning of various negations in logic programming. It is shown that the failure operator FP is a dual of the TP, immediate consequence operator developed by Van Emden and Kowalski and is downward continuous. It has the desirable properties entirely analogous to what TP has such as continuity, having a unique least fixpoint and a unique greatest fixpoint. It provides natural proof theories for various version negations in logic programming. We prove that set complementation provides the isomorphism between the fixpoints of FP and those of TP, which illustrates the duality of FP and TP. The existing treatment of negation in logic programming can be given in a simple and elegant fixpoint characterization