Negation in Logic Programming. (English) Zbl 0718.68020

Shepherdson, J. C.

Foundations of deductive database and logic programming, 19-88 (1988).

[For the entire collection see Zbl 0699.68009.]
The paper provides an extensive overview on the use of negation in logic programming, summarizes developments and discuss the relationship among various approaches. It describes major results on elimination of negation by renaming, on definite Horn programs with general queries, on fixpoint models, on the relation between closed world assumption and completed databases, on negation as failure and on negation for special classes. Since classical negation in logic programs and queries is very time- consuming or not useful, several notions of negation according to some kind of declarative semantics for logic programming are introduced. The three different semantics are: the least fixpoint by Herbrand models which are obtained by starting with the empty clause and closing under the operation of adding those ground atoms that are derivable, closed world assumption assuming that the program contains all positive information about the objects and the completed database which is obtained by assuming that the heads are equivalent to the disjunction of the bodies of all clauses with the same head. Two fundamental principles are to be observed and all kinds of negation should be measured against these principles: First, the semantics of negation should be clear and easy intelligible, and second, the syntax should be computable.
There are three special cases where full classical negation can be easily implemented: elimination of negation by renaming, definite Horn programs with general queries and general Horn programs with definite or negative queries. Then the paper considers in detail the three declarative semantics. Several consistency conditions are discussed and proved. The relationship between the closed world assumption and completed databases is considered. Since the consistency of one kind does not imply the consistency of the other kind and since the union of both kinds can lead to inconsistency for consistent closures of the two kind conditions under which the union of both kinds is consistent are in detail discussed.
The rest of the paper discusses three treatments of negation. Firstly, negation as failure means the result of adding negation as failure to SLD-resolution. It is sound with respect to the completion and also with respect to the closed world assumption. Under certain restrictions it is complete with respect to the completed database. Secondly, semantics of negation in an indefinite database can be defined by the generalized closed world assumption. Thirdly, semantics for negation as failure in terms of 3-valued logic for completed databases is discussed.

Reviewer: B.Thalheim (Rostock)

MSC:

68N17	Logic programming
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35	Mechanization of proofs and logical operations

Keywords:

nonmonotonic reasoning; negation in logic programming; Horn programs; fixpoint models; closed world assumption; completed databases; negation as failure

Citations:

Zbl 0699.68009