Declarative Logic Programming. Michael Kifer

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 t₁, …, tk are terms and f ∈ σ is a k-ary function symbol, then f(t₁, …, tk) is also a term.

      An atom is an expression p(t₁, …, tk), where p ∈ σ is a k-ary predicate symbol and t₁, …, 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) b₁, …, bm, not c₁, …, 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 = b₁, …, bm, not c₁, …, not cn of literals we define B⁺ = {b₁, …, bm} and B⁻ = {c₁, …, 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.