On the declarative and procedural semantics of logic programs

Mechanization of proofs and logical operations (03B35) Properties of classes of models (03C52) Models of other mathematical theories (03C65) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

One of the most challenging problems in Logic Programming (further LP for short) is the problem of finding a suitable formalization of the type of non-monotonic reasoning used in LP. The new semantics for LP based on the class of the so-called perfect models is introduced. Analyzing the existing semantics for LP such as Clarke's completion, the least Herbrand model semantics, minimal model semantics, the author points out the universal and existential query problems arising with these semantics as well as their inability to capture the non-monotonic character of reasoning used in LP when non-positive logic programs are considered. The perfect model semantics is based on the ordering \(``<\) of predicates and preference \(``<<\) between models. Let M and N be two distinct not necessarily Herbrand models of a general program P with the same universe and the same interpretations of function symbols. Let Em(A) denote the extension of a predicate A in M. We say that M is preferable to N \((M\ll N)\) iff for every predicate A with non- empty Em(A)\(\setminus En(A)\) there is a predicate \(B>A\) such that the set En(B)\(\setminus Em(B)\) is not empty. Perfect models are the models minimal w.r.t. the \(``\ll \cdot relation\). The perfect model semantics combines desirable features of previous approaches and eliminates some of their drawbacks. Moreover, the perfect model semantics is shown to be equivalent to the four major formalizations of non-monotonic reasoning in artificial intelligence: McCarthy's circumscription, Reiter's closed world assumption, Moore's autoepistemic logic and Reiter's default theory. Still for positive logic programs the classes of perfect models and minimal models coincide. The new procedural semantics for general logic programs called SLS-resolution (Linear resolution with selection function for stratified programs) is introduced and validated. The SLS- resolution is a natural generalization of SLD-resolution (Linear resolution with selection for definite programs). It is proved that SLS- resolution is sound and complete w.r.t. perfect model semantics. The paper is clearly written, supplied with large number of good examples and precise proofs, which makes it easily understandable by both experts and novices in the field of LP.

Recommendations

Cited in

(44)

This page was built for publication: On the declarative and procedural semantics of logic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1823724)