Negation in logic programming. (English) Zbl 0655.68018

Kunen, Kenneth

J. Logic Program. 4, 289-308 (1987).

The most familiar approach to negation in logic programming is the closed data base (CDB) approach by K. Clark. It does not satisfy the author since it disagrees with most PROLOG interpreters even in some simple cases. A new semantics is proposed here which is a truncation of M. Fitting’s [ibid. 2, 295-312 (1985; Zbl 0589.68011)] 3-valued semantics before the level w. This is proved to be recursively enumerable using decidability of (in fact quantifier elimination for) the equational theory CET which postulates axioms of unification (values of different functions are unequal, every function is 1-1, etc.). Equivalent definition is truth in all (not only Herbrand) 3-valued models of CET where equality is 2-valued. A lot of useful remarks is made.

Reviewer: G.Mints

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68Q65	Abstract data types; algebraic specification
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

negation; logic programming; PROLOG; interpreters; 3-valued semantics; decidability; quantifier elimination; equational theory

Citations:

Zbl 0589.68011