Document Type
Report
Date
3-1991
Keywords
Logic programming
Language
English
Disciplines
Computer Sciences
Description/Abstract
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.
Recommended Citation
Yang, Feng, "Duality in Logic Programming" (1991). Electrical Engineering and Computer Science - Technical Reports. 119.
https://surface.syr.edu/eecs_techreports/119
Source
local
Additional Information
School of Computer and Information Science, Syracuse University, SU-CIS-91-10