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) 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:
?- 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.
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 ?
Trying to get my head around the advantages and disadvantages of WFS, ASP and sCASP …
?- 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.
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
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 (?).
Trying to get my head around the advantages and disadvantages of WFS, ASP and sCASP …
I would be very interested in reading about your conclusions about this topic. In a future paper ?
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.
