slx: Extended Logic Programs under the Well-Founded Semantics

As explained in the section Using Tabling in XSB, XSB can compute normal logic programs according to the well-founded semantics. In fact, XSB can also compute Extended Logic Programs, which contain an operator for explicit negation (written using the symbol - in addition to the negation-by-failure of the well-founded semantics (\+ or not). Extended logic programs can be extremely useful when reasoning about actions, for model-based diagnosis, and for many other uses [2]. The library, slx provides a means to compile programs so that they can be executed by XSB according to the well-founded semantics with explicit negation [1]. Briefly, WFSX is an extension of the well-founded semantics to include explicit negation and which is based on the coherence principle in which an atom is taken to be default false if it is proven to be explicitly false, intuitively:

- p $$\Rightarrow$$ not p.

This section is not intended to be a primer on extended logic programming or on WFSX semantics, but we do provide a few sample programs to indicate the action of WFSX. Consider the program

s:- not t.

t:- r.
t.

r:- not r.

If the clause -t were not present, the atoms r, t, s would all be undefined in WFSX just as they would be in the well-founded semantics. However, when the clause t is included, t becomes true in the well-founded model, while s becomes false. Next, consider the program

s:- not t.

t:- r.
-t.

r:- not r.

In this program, the explicitly false truth value for t obtained by the rule -t overrides the undefined truth value for t obtained by the rule t:- r. The WFSX model for this program will assign the truth value of t as false, and that of s as true. If the above program were contained in the file test.P, an XSB session using test.P might look like the following:

              > xsb
              
              | ?- [slx].
              [slx loaded]
            
              yes
              | ?- slx_compile('test.P').
              [Compiling ./tmptest]
              [tmptest compiled, cpu time used: 0.1280 seconds]
              [tmptest loaded]
            
              | ?- s.
              
              yes
              | ?- t.

              no
              | ?- naf t.
              
              yes
              | ?- r.

              no
              | ?- naf r.
              
              no
              | ?- und r.
              
              yes

In the above program, the query ?- t. did not succeed, because t is false in WFSX: accordingly the query naf t did succeed, because it is true that t is false via negation-as-failure, in addition to t being false via explicit negation. Note that after being processed by the SLX preprocessor, r is undefined but does not succeed, although und r will succeed.

We note in passing that programs under WFSX can be paraconsistent. For instance in the program.

              p:- q.

              q:- not q.
              -q.

both p and q will be true and false in the WFSX model. Accordingly, under SLX preprocessing, both p and naf p will succeed.

slx_compile(+File)

slx
Preprocesses and loads the extended logic program named File. Default negation in File must be represented using the operator not rather than using tnot or \+. If L is an objective literal (e.g. of the form A or - A where A is an atom), a query ?- L will succeed if L is true in the WFSX model, naf L will succeed if L is false in the WFSX model, and und L will succeed if L is undefined in the WFSX model.