%% The following simple program shows that incremental tabling does not always
%% update all tables correctly.
/ Please see explanations inline /
:- dynamic p/1, neg_p/1 as incremental.
:- table q/1, defeated/1 as incremental.
:- import incr_assert/1 from increval.
bb(x).
cc(a).
q(X) :- bb(X).
q(X) :- p(X).
defeated(p(X)) :- cc(X), clause(neg_p(),).
/
Only q(X) :- bb(X) can fire, so Attempt 1 prints only
q = x -- correct/
?- writeln('Attempt 1:'), (q(X), writeln(q=X), fail ; true).
/
Now q(X) :- p(X) :- cc(X), X=a can fire.
Also, defeated(p(X)) is false, since clause(neg_p(),) is false.
So, Attempt 2 will print
q = a -- correct
q = x -- correct/
?- incr_assert((p(X):-cc(X),tnot(defeated(p(X))))).
?- writeln('Attempt 2:'), (q(X), writeln(q=X), fail ; true).
/*
Now neg_p(X) becomes a head of a clause. So, defeated(p(a)) is true.
Therefore, p(a) now becomes false, so q(a) should be false.
Attempt 3 should be printing
q = x
but instead prints both
q = a -- wrong!!!
q = x -- correct
** This is an incremental tabling problem. Indeed, the next
abolish_all_tables and subsequent Attempt 4 should that when tables
are cleared out then it would print only q = x./
?- incr_assert(neg_p(a)).
?- writeln('Attempt 3:'), (q(X), writeln(q=X), fail ; true).
/ Only after abolishing we are getting a correct result. /
?- abolish_all_tables.
?- writeln('Attempt 4:'), (q(X), writeln(q=X), fail ; true).
I don't consider this a bug for now, because ...
If you make the change:
%defeated(p(X)) :- cc(X), clause(neg_p(),).
defeated(p(X)) :- cc(X), neg_p(Y).
Things work fine -- at least in the SVN version. The problem is that the clause/2 isn't really considered a call in terms of creating the call dependency graph. In fact, I think it should be, unless there is some compelling case that I'm missing. So I'll close it out.
Problem was with the use of clause/2. Closing for now.
the problem is that for defeasible reasoning one needs to do metaprogramming.
I am not sure this is relevant at present, but maybe it should be reclassified as a wish list?