
doi: 10.1007/bf00243002
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 \(``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.
Mechanization of proofs and logical operations, Properties of classes of models, Specification and verification (program logics, model checking, etc.), SLD-resolution, Logic Programming, Herbrand models, SLS-resolution, non-monotonic logic, declarative and procedural semantics, Models of other mathematical theories, Theorem proving (deduction, resolution, etc.)
Mechanization of proofs and logical operations, Properties of classes of models, Specification and verification (program logics, model checking, etc.), SLD-resolution, Logic Programming, Herbrand models, SLS-resolution, non-monotonic logic, declarative and procedural semantics, Models of other mathematical theories, Theorem proving (deduction, resolution, etc.)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 76 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 1% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
