tnot/1 vs. ${\tt '\backslash+'\!/1}$

Subject to some semantic restrictions, an XSB programmer can intermix the use of tabled negation (tnot/1) with Prolog's negation ( ${\tt '\backslash+'\!/1}$, or equivalently fail_if/1 or not/1). These restrictions are discussed in detail below -- for now we focus on differences in behavior or these two predicates in stratified programs. Recall that ${\tt '\backslash+'(S)}$ calls $S$ and if $S$ has a solution, Prolog executes a cut over the subtree created by ${\tt '\backslash+'(S)}$, and fails. tnot/1 on the other hand, does not execute a cut, so that all subgoals in the computation path begun by the negative call will be completely evaluated. The major reason for not executing the cut is to insure that XSB evaluates ground queries to Datalog programs with negation with polynomial data complexity. As seen [15], this property cannot be preserved if negation ``cuts'' over tables.

There are other small differences between tnot/1 and ${\tt '\backslash+'\!/1}$ illustrated in the following exercise.

Exercise 5.3.3   In general, making a call to non-ground negative subgoal in Prolog may be unsound (cf. [42]), but the following program illustrates a case in which non-ground negation is sound.

ngr_p:- \+ ngr_p(_).
ngr_p(a).

One tabled analog is

:- table ngr_tp/1.
ngr_tp(a).

ngr_tp:- tnot(ngr_tp(_)).

Version 3.0 of XSB will flounder on the call to ngr_tp, but not on the call to ngr_p/0. On the other hand if sk_not/1 is used

ngr_skp:- sk_not(ngr_tp(_)).

the non-ground semantics is allowed.

sk_not/1 works by asserting a new tabled subgoal, abstractly

:- table '_$ngr_tp'
'_$skolem_ngr_tp' :- ngr_tp(_).

to avoid the problem with variables. In addition, since sk_not/1 creates a new tabled predicate, it can be used to call non-tabled predicates as well, ensuring tabling.

The description of tnot/1 in Section 6.5 describes other small differences between ${\tt '\backslash+'\!/1}$ and tnot/1 as implemented in XSB. Before leaving the subject of stratification, we note that the concepts of stratification also underly XSB's evaluation of tabled findall: tfindall/3. Here, the idea is that a program is stratified if it contains no loop through tabled findall (See the description of predicate tfindall/3 on page ).