A natural semantics for logic programs with negation

Abstract

Two natural ways to specify the declarative semantics of logic programs and deductive databases are the fixpoint theory of Van Emden and Kowalski [11] and Clark's predicate completion [2]. The fixpoint theory does not apply to general programs with negation; a generalization of the theory can be defined [1,12] only if the programs are stratified. Clark's predicate completion is defined for logic programs with negation. In general, it fails to capture their intended semantics [7,8,9]. In this paper, we introduce a new notion of quasi-interpretation as a set of ground clauses of the form A ← ¬ B1,.., ← Bn and extend the classic fixed point theory in [11] to quasi-interpretations. The semantics of a logic program P is defined by Clark's predicate completion of the least fixpoint of a continuous operator TP on quasi-interpretations. It is called the fixpoint completion of P, fixcomp(P). We then discuss the relations between fixcomp(P) and other approaches [5,7,8,9].