Authors/Contributors

Feng Yang

Document Type

Report

Date

3-1991

Embargo Period

5-2-2012

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.

Additional Information

School of Computer and Information Science, Syracuse University, SU-CIS-91-10

Source

local

Share

COinS
 
 

To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.