Declarative Logic Programming. Michael Kifer
Читать онлайн книгу.
can be stratified [Apt et al. 1988, Van Gelder 1989] in such a way that whenever a first goal depends negatively on a second goal, the second goal is in a strictly lower stratum than the first, then we can compute the goals in order from lower strata to higher strata. For example, consider the program:
We can assign a stratum to each proposition, as, for example, t:1, r:2, s:3, q:3, and p:4. Then every proposition depends positively on other propositions at its stratum or lower, and depends negatively on propositions only at strictly lower strata. So p depends negatively on q and q is at a lower stratum than p. Propositions q and s depend on each other positively and have the same stratum. For such stratified programs, we can compute the meanings of propositions by starting with the propositions of the lowest stratum and then moving to the next higher stratum. Thus, when the negation of a proposition is needed, it has already been completely evaluated at a previous stratum. This stratum-by-stratum fixed point, which is called the perfect model of the program [Przymusinski 1988b], defines the semantics for stratified programs. A key point in this definition is how to precisely define when a goal depends on another goal. Initially the notion of predicate stratification was defined that used the static predicate call graph to determine potential goal dependencies. The introductory example, along with the rule for unrelated above, is predicate-stratified, with person, related, and advised in the first stratum and unrelated in the second stratum. However, many meaningful, useful programs were not predicate-stratified, but still did not have real recursion through negation and could be given reasonable meanings. So a second, more refined, definition of stratification, called local stratification [Przymusinski 1988a], was proposed, but the same situation occurred. Thus, dynamically stratified [Przymusinski 1989] and yet more definitions were proposed. It was generally agreed that all forms of stratification gave appropriate semantics for the programs to which they applied, but a semantics that worked for all programs with negation was desired.
Two general solutions followed: the Well-Founded Semantics [Van Gelder et al. 1991] and the Stable-Model Semantics [Gelfond and Lifschitz 1988]. There have been (many) others, but these two have had the most acceptance and influence. We will discuss them in turn. For a detailed treatment of this topic, see Chapter 2.
The Well-Founded Semantics (WFS) uses a three-valued logic, in which goals can be true, false, or undefined. The WFS can be defined by an iterated fixed point, which at each iteration computes facts that must be true and facts that must be false. When the computation converges, facts that are neither determined true nor false are undefined. In this manner, a three-valued well-founded model can be constructed for every program. If the program is stratified (for any of the forms of stratification), the well-founded model will be two valued and agree with the perfect model.
For the program
the fact teaches_db(maier) is undefined in the WFS. And for the program
all facts are undefined in the WFS. The well-founded model is polynomially computable in the size of the ground program, and has polynomial data complexity for Datalog programs. The WFS satisfies the “relevancy” property, in that the truth value of a goal depends only on goals it depends on in the goal-dependency graph. Thus, there is a goal-directed, top-down evaluation strategy for the well-founded semantics that is worst-case quadratic in the size of the ground program [Chen and Warren 1996]. We discuss the most popular such strategy in Section 1.5.
The other definition is the Stable-Model Semantics (SMS). Stable models are two-valued, and a Datalog program may have multiple stable models, or it may have none. A stable model is defined as a model that has the property that, if all negative goals in the (ground) Datalog program are interpreted as true or false according to the model and the program is then simplified accordingly, then the minimum model of the resulting positive program is that original model.
For instance, the program
has no stable models, but the program
has the following two stable models:
Finding a stable model is in general NP-hard in the size of the (ground) program. Also, there is no obvious goal-directed way to compute a stable model; the entire program may have to be processed, since an inconsistency (e.g., a rule p :- not p) anywhere in the program means the entire program has no stable model. A rule such as p :- q, not p. (where p appears nowhere else in the program) implies that q must be false in any stable model, regardless of how q might be defined elsewhere in the program.
The AI community was most interested in the SMS, which was defined by Gelfond and Lifschitz [1988], who came from theoretical AI. The general idea of assuming false what is not known to be true is known as the “closed world assumption” [Reiter 1977b]. It can be interpreted as a kind of common-sense reasoning and has close ties to nonmonotonic logic formalisms that had been studied previously in the AI community [Bobrow 1980, Brewka et al. 1997] by John McCarthy, Drew McDermott, Jon Doyle, Ray Reiter, and Robert Moore, among many others. Since many AI formalisms inherently have high complexity, the fact that SMS was NP-hard was not seen as a particular problem. Datalog under the SMS led to the exploration of some traditional AI problems, such as planning and reasoning about change and actions.
The database community was more interested in WFS, which was defined by Van Gelder et al. [1991], who were researchers in the theoretical database community. Its computational properties conformed much more to traditional database requirements. Some have constrained their interest to Datalog programs that have two-valued well-founded models, which can be considered as the strongest definition possible for stratified programs.
The logic programming community has shown interest in both definitions, but probably more in the SMS. SMS has spawned a large subcommunity that studies Answer-Set Programming (ASP) [Marek and Truszczyński 1999]. The idea is to use Datalog under SMS as a “programming language” to specify sets of propositions, i.e., those determined as true in some stable model of the program. Many combinatorial problems can be naturally specified by such Datalog programs. ASP also allows disjunction in the rule heads—an extension inspired by the earlier work on disjunctive logic programming [Minker 1994, Minker and Seipel 2002]. It is shown in Eiter et al. [1997] that this extension adds both the expressive power and complexity to the language. Much research has gone into developing efficient solvers that can find one or all of the stable models of a Datalog program. ASP is closely related to SAT solving, i.e., finding truth assignments that satisfy a set of propositional formulas. The difference is that an ASP solver will find only “minimal” satisfying truth assignments,8 and for this reason they may be better suited to problems where minimality is important, such as planning. Planning is often formulated as reachability in a graph whose nodes are states and whose edges are possible actions, and formulating reachability using logic rules requires minimality.
There have been proposals for integrating the desirable aspects of WFS and SMS into a single framework. Of particular interest is FO(ID) [Denecker et al. 2001, Vennekens et al. 2010] and, more recently, the founded semantics [Liu and Stoller 2018]. This line of work may eventually provide the basis for a broadly accepted integrated semantics for Datalog.
1.4.2 Arithmetic and Other Evaluable Predicates
As presented so far, Datalog is limited to symbolic