Читать книгу Declarative Logic Programming - Michael Kifer - Страница 12
Оглавление2
An Introduction to the Stable and Well-Founded Semantics of Logic Programs
Miroslaw Truszczynski
This chapter provides a brief introduction to two main semantics of logic programs with negation, the stable-model semantics of Gelfond and Lifschitz, and the well-founded semantics of Van Gelder, Ross, and Schlipf. We present definitions, introduce basic results, and relate the two semantics to each other. We restrict attention to the syntax of normal logic programs and focus on classical results. However, throughout the chapter and in concluding remarks we briefly discuss generalizations of the syntax and extensions of the semantics, and mention several recent developments.
2.1 Introduction
The roots of logic programming can be traced back to efforts to build resolutionbased automated theorem provers in the mid-1960s [Robinson 1965]. A realization that resolution can turn Horn theories into programs came about in the early 1970s and rested on the foundational work of Kowalski and Kuehner [1971] and Kowalski [1974], as well as the implementation effort of Colmerauer and his research group, in which the Prolog programming language was developed [Colmerauer et al. 1973].
Negation was present in Prolog from the very beginning. Its meaning was specified operationally through its implementation. However, for almost two decades, finding a satisfactory declarative account of negation was elusive. The first significant progress was obtained by Clark, who proposed reading programs as definitions and formalized that reading by means of the program completion [Clark 1978]. A different plan of attack was developed a few years later by Apt, Blair, and Walker [1988] and, independently, by Przymusinski [1988a, 1988b]. They introduced a large and natural class of programs with negation, called stratified programs, and showed that the meaning of a stratified program is captured by a certain well-motivated Herbrand model. Przymusinski [1988a] called this model perfect. Soon thereafter, Gelfond and Lifschitz [1988] proposed the stable-model semantics and Van Gelder et al. [1988, 1991] the well-founded semantics. The stable-model semantics was strongly influenced by research in knowledge representation concerned with the notion of nonmonotonic reasoning, and built on the semantics of default logic by Reiter [1980] and autoepistemic logic by Moore [1985]. The well-founded semantics followed the query-evaluation paradigm of Prolog but framed it in a three-valued setting. Both semantics were heavily influenced by the perfect-model semantics and can be regarded as its generalizations to the class of all programs. Moreover, despite some fundamental differences, they also show strong and interesting connections to the completion semantics by Clark.
The stable-model and the well-founded semantics have had major implications on the fields of logic programming and knowledge representation. Since their inception, they fueled research in these two fields and gave rise to fascinating theoretical results, implementations of declarative programming languages, and successful applications. In particular, the answer-set programming paradigm [Marek and Truszczyński 1999, Niemel¨a 1999, Brewka et al. 2011] and its modern implementations trace their roots to the stable-model semantics [Gebser et al. 2012], while some closely related declarative programming systems grew out of generalizations of the well-founded semantics [Denecker 2009]. The latter underlies also a successful Prolog descendant, the XSB system [Sagonas et al. 1994], and several other systems we mention later on.
In this tutorial presentation, we introduce the two semantics and show that, despite their differences, they are closely related. Our goal is to present basic properties of the stable-model and the well-founded semantics, focusing on the most significant lines of research. After introducing the terminology and the most essential preliminaries, we start our presentation with the case of Horn programs (Section 2.3). In Section 2.4 we discuss several examples that point out problems that arise for programs with negation, and informally suggest ways in which these problems could be addressed. We follow up with a formal discussion of the stablemodel semantics as an extension of the least-model semantics of Horn programs to the case of programs with negation (Section 2.5). The key topics we discuss are stratification and program splitting, supported models, completion, tight programs, loops and the Loop Theorem, and strong equivalence of programs. We then change gears and move into the realm of four-valued Herbrand interpretations. While there, we define partial stable and partial supported models, and the most distinguished representatives of the two classes of “partial” models: the well-founded and the Kripke-Kleene models, respectively (Section 2.6). We conclude with brief closing comments.
2.2 Terminology, Notation, and Other Preliminaries
Logic Programming
The language of logic programming is determined by a countable vocabulary σ consisting of function and predicate symbols, each assigned a non-negative arity. Function symbols of arity 0 are called constant symbols. We assume that σ contains at least one constant symbol. Expressions of the language may also contain variable symbols. They come from a fixed infinite countable set Var that does not depend on σ. In other words, the same set of variables is used with every vocabulary.
The terms of the language are defined in the same way as in the first-order logic: all constant and variable symbols are terms and, if t1, …, tk are terms and f ∈ σ is a k-ary function symbol, then f(t1, …, tk) is also a term.
An atom is an expression p(t1, …, tk), where p ∈ σ is a k-ary predicate symbol and t1, …, tk are terms. Thus, atoms in logic programming are of the same form as atomic formulas in the language of first-order logic.
Terms and atoms that have no occurrences of variable symbols are ground. The Herbrand universe comprises all ground terms of the language and the Herbrand base comprises all ground atoms. One of the connectives in the language of logic programming is the negation connective not. Negation is applied only to atoms. Atoms and negated atoms are called literals. Rules are expressions constructed from literals by means of the rule connective “←” and the conjunction connective “,”. More precisely, a rule (sometimes called a clause) is an expression of the form
where a and all bi’s and cj’s are atoms. The atom a is the head of the rule (2.1) and the conjunction (list) b1, …, bm, not c1, …, not cn of literals is its body. If r denotes a rule, we write H(r) and B(r) for the head and the body of r, respectively. We extend this notation to programs and write H(P) and B(P) for the sets of heads and bodies of rules in a program P.
We often write rules as a ← B, where a is an atom and B is a list of literals. For every list B = b1, …, bm, not c1, …, not cn of literals we define B+ = {b1, …, bm} and B− = {c1, …, cn}, and we often specify a rule a ← B as a ← B+, not B−. We note a slight abuse of the notation here. The expression in the body, B+, not B−, is not a list but a pair of sets. Nevertheless, as all semantics of logic programs we consider in this chapter are insensitive to the order of literals in the bodies of rules, the notation gives all essential information about the rule it describes.
If n = 0, rule (2.1) is a Horn rule and if m + n = 0, a fact. In the latter case, we omit ‘←’ from the notation, that is, we write a instead of a ←. A logic program (or just a program) is a collection of rules. A Horn program is a program consisting of Horn rules.
