Negation in logic programming. (English) Zbl 0655.68018

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


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


Zbl 0589.68011
Full Text: DOI