Before considering the full well-founded semantics, we discuss how XSB can be used to evaluate programs with stratified negation. Intuitively, a program uses stratified negation whenever there is no recursion through negation. Indeed, most programmers, most of the time, use stratified negation.
win(X):- move(X,Y),tnot(win(Y)).
is stratified when the move/2 relation is a binary tree. To see
this, load the files tree1k.P and
table_examples.P from the directory
$XSB_DIR/examples and type the query
?- win(1).
win(1) calls win(2) through negation, win(2) calls
win(4) through negation, and so on, but no subgoal ever calls
itself recursively through negation.The previous example of win/1 over a binary tree is a simple instance of a stratified program, but it does not even require tabling. A more complex example is presented below.
lrd_p:- lrd_q,tnot(lrd_r),tnot(lrd_s). lrd_q:- lrd_r,tnot(lrd_p). lrd_r:- lrd_p,tnot(lrd_q). lrd_s:- tnot(lrd_p),tnot(lrd_q),tnot(lrd_r).Should lrd_s be true or false? Try it in XSB. Using the intuitive definition of ``stratified'' as not using recursion through negation, is this program stratified? Would the program still be stratified if the order of the literals in the body of clauses for lrd_p, lrd_q, or lrd_r were changed?
The rules for p, q and r are involved in a positive loop, and no answers are ever produced. Each of these atoms can be failed, thereby proving s. Exercise 5.3.2 thus illustrates an instance of how tabling differs from Prolog in executing stratified programs since Prolog would not fail finitely for this program.
