1.0.0.0.1 Well-Founded Semantics

To understand the implications of SLG resolution [15], recall that Prolog is based on a depth-first search through trees that are built using program clause resolution (SLD). As such, Prolog is susceptible to getting lost in an infinite branch of a search tree, where it may loop infinitely. SLG evaluation, available in XSB, can correctly evaluate many such logic programs. To take the simplest of examples, any query to the program:

:- table ancestor/2.

ancestor(X,Y) :- ancestor(X,Z), parent(Z,Y).
ancestor(X,Y) :- parent(X,Y).

will terminate in XSB, since ancestor/2 is compiled as a tabled predicate; Prolog systems, however, would go into an infinite loop. The user can declare that SLG resolution is to be used for a predicate by using table declarations, as here. Alternately, an auto_table compiler directive can be used to direct the system to invoke a simple static analysis to decide what predicates to table (see Section 3.10.4). This power to solve recursive queries has proven very useful in a number of areas, including deductive databases, language processing [36,37], program analysis [20,16,7], model checking [45] and diagnosis [29]. For efficiency, we have implemented SLG at the abstract machine level so that tabled predicates will be executed with the speed of compiled Prolog. We finally note that for definite programs SLG resolution is similar to other tabling methods such as OLDT resolution [56] (see Chapter 5 for details).

Example 1.0.1   The use of tabling also makes possible the evaluation of programs with non-stratified negation through its implementation of the well-founded semantics [57]. When logic programming rules have negation, paradoxes become possible. As an example consider one of Russell's paradoxes -- the barber in a town shaves every person who does not shave himself -- written as a logic program.

 
:- table shaves/2.

shaves(barber,Person):- person(Person), tnot(shaves(Person,Person)).
person(barber).
person(mayor).

Logically speaking, the meaning of this program should be that the barber shaves the mayor, but the case of the barber is trickier. If we conclude that the barber does not shave himself our meaning does not reflect the first rule in the program. If we conclude that the barber does shave himself, we have reached that conclusion using information beyond what is provided in the program. The well-founded semantics, does not treat shaves(barber,barber) as either true or false, but as undefined. Prolog, of course, would enter an infinite loop. XSB's treatment of negation is discussed further in Chapter 5.