 # Unexplained behaviour wrt the well founded semantics - Part 4

Hi Jan, Hi all,

I come back with something else I do not understand related to the well founded semantics (WFS).

I’m using version: 8.3.29-4-g836862aeb

I would like to differenciate atoms that are undefined (according to WFS), from those that are true, from those that are false. Thus I define the following predicates:

``````isUndefined(Atom):- Atom,tnot(Atom).

isTrue(Atom):-	\+ (Atom,tnot(Atom)), Atom.

isFalse(Atom):- \+ (Atom,tnot(Atom)), \+Atom.
``````

The idea is the following:

• isUndefined(Atom) returns true if and only if Atom returns undefined
• isTrue(Atom) returns true if and only if Atom returns true
• isFalse(Atom) returns true if and only if Atom returns false

The implementation given above seems to be correct and to behave well with a ground Atom. When Atom is not ground however, the expected result is not obtained as illustrated below. I have the following program:

``````:- table p/1.

q(1).
r(3).

p(X) :- r(X),tnot(p(X)).
p(X) :- q(X).
``````

What I’m getting is:

``````?- p(1). p(2). p(3).

true.

false.

% WFS residual program
p(3) :-
tnot(p(3)).
p(3).

?- isTrue(p(1)). isFalse(p(1)). isUndefined(p(1)).

true.

false.

false.

?- isTrue(p(2)). isFalse(p(2)). isUndefined(p(2)).

false.

true.

false.

?- isTrue(p(3)). isFalse(p(3)). isUndefined(p(3)).

false.

false.

% WFS residual program
p(3) :-
tnot(p(3)).
(tnot(p(3)), p(3)).

?- findall(X,p(X),Result).
Result = [3, 1].

?- isTrue(p(X)).
false.
``````

Everything is correct except the last result where I expected

``````X = 1
``````

Is there something I have not understood ?

Best regards

It is not so hard to explain:

``````?- p(X), tnot(p(X)).
% WFS residual program
p(3) :-
tnot(p(3)).
X = 3,
(tnot(p(3)), p(3)) ;
``````

And thus the NAF negation `\+/1` is false. I thought you could maybe work around this using not_exists/1, but this too seems to fail. Don’t know why (yet). What does work is

``````isTrue(Atom):-	Atom, \+ (Atom,tnot(Atom)).
``````

A simpler way to distinguish undefined from true results is to use call_delays/2.

1 Like

The most sensible definitions I can come up with are

``````isUndefined(Atom) :- call_delays(Atom, Delays), Delays \== true.
isTrue(Atom)      :- call_delays(Atom, true).
isFalse(Atom)     :- \+ isTrue(Atom).
``````

That works fairly well, except that isFalse/1 requires a ground argument to avoid floundering. You need constructive negation. sCASP can do that. Still learning, I tried. sCASP on

``````q(1).
r(3).

p(X) :- r(X), not p(X).
p(X) :- q(X).
``````

gives “no models” on every query though because our knowledge base is inconsistent. If we delete the inconsistent first clause for p/1 we get

``````?- not p(X).

MODEL:
{ not q(X | {X \= 1}),  not p(X | {X \= 1}) }

BINDINGS:
X \= 1 ?
``````

1 Like

``````?- p(X), tnot(p(X)).
% WFS residual program
p(3) :-
tnot(p(3)).
X = 3,
(tnot(p(3)), p(3)) ;
``````

And thus the NAF negation `\+/1` is false.

I understand my mistake !

What does work is

``````isTrue(Atom):-	Atom, \+ (Atom,tnot(Atom)).
``````

Clever !

A simpler way to distinguish undefined from true results is to use call_delays/2.

I realize I am not comfortable with this predicate call_delays, and also with others like call_residual_program/2, delays_residual_program/2, not_exists/1, tabled_call/1, current_table/2. So I have to go back to work. Thank you !

I think I have understood the purpose of call_delays now. Just to be sure with my own words : call_delays(Atom, Delays) is globally true, only if we have: (Delays is true) implies (Atom is true). Is that ok ?

The most sensible definitions I can come up with are

``````isUndefined(Atom) :- call_delays(Atom, Delays), Delays \== true.
isTrue(Atom)      :- call_delays(Atom, true).
isFalse(Atom)     :- \+ isTrue(Atom).
``````

I agree with your definitions. I just cannot see the difference with:

``````isUndefined(Atom):- Atom,tnot(Atom).
isTrue(Atom):- Atom, \+ (Atom,tnot(Atom)).
isFalse(Atom):- \+Atom.
``````

Is it a performance issue ?
Anyway, there is still the necessity to give a ground argument to isFalse/1.

You need constructive negation. sCASP can do that. Still learning, I tried. sCASP on

``````q(1).
r(3).

p(X) :- r(X), not p(X).
p(X) :- q(X).
``````

gives “no models” on every query though because our knowledge base is inconsistent. If we delete the inconsistent first clause for p/1 we get

``````?- not p(X).

MODEL:
{ not q(X | {X \= 1}),  not p(X | {X \= 1}) }

BINDINGS:
X \= 1 ?
``````

This is very interesting ! I was not aware of sCASP and its constructive negation. It would be great to include it inside WFS… Maybe some papers are dealing of this (?).

Thank you very much Jan !

I think so, though I’m not 100% sure I get what you are saying. call_delays/2 is true if call(Atom) is true under the conditions imposed by Delays. If Delays is `true`, this means call(Atom) is unconditionally true. Otherwise it is an opaque representation of the delays (i.e., condition under which the atom is true). Does that make sense?

Yes. Although the impact may be fairly small as tnot always works on an already complete table. You’d have the measure (and maybe performance is irrelevant to you anyway ).

Of, this is the same as `isTrue(Atom) :- Atom, \+ tnot(Atom).` CASP, implementing stable model semantics and tabling with WFS are quite different beasts. I not a logician …

Search Google Scholar for “scasp gupta” and you have most papers. sCASP was written by Joaquin Arias. Gopal Gupta has co-authored most of the papers concerning sCASP and its predecessor sASP. The SWI-Prolog port as at GitHub - JanWielemaker/sCASP: top-down interpreter for ASP programs with constraints. The original version in Ciao is primarily a stand-alone system. I’m working on turning this into an embedded language, i.e., allow solving a specific query under sCASP semantics.

2 Likes

Yes !

Yes, performance is of great interest for me. So I keep your solution !

You’re right, of course.

I meant including constructive negation only into WFS. But maybe this is inherently associated to stable models. I’m not a logician either.

That will be very useful to have such an embedded language.

Hi Jan,

just a little remark on a past post:

After a few tests, my colleague Sylvain Lapeyrade found a problem with the last two rules :

``````isTrue(Atom)      :- call_delays(Atom, true).
isFalse(Atom)     :- \+ isTrue(Atom).
``````

since if Atom is undefined, then isFalse(Atom) is true (whereas we would like false). So we changed by

``````isUndefined(Atom) :- call_delays(Atom, Delays), Delays \== true.
isTrue(Atom)      :- call_delays(Atom, true).
isFalse(Atom)     :- \+ Atom.
``````

It seems to be ok.

Best regards

Christophe

1 Like