Problem using abduction over disunity rules in s(CASP)

Help!
1

If I create a rule in s(CASP) that requires a disunity between two variables, s(CASP) cannot reason abductively over that rule unless all but one of the disunified terms is stated in the program.

I have a swish file demonstrating the problem, linked below. The only workaround I can think of is ugly, fragile, and makes a mess of the models and explanations.

Abduction seems to work with disunity as long as all-but-one of the disunified terms are not abduced.

https://swish.swi-prolog.org/p/abduction_over_disjunction.swinb

Is there some way to get s(CASP) to cooperate? Is there perhaps a different way of expressing disunities that s(CASP) is able to navigate better? I have heard people say you should prefer dif(X,Y) to X \= Y, but dif gives a permission error in swish, so I don’t know if it would work.

As an aside, I note the s(CASP) github repository under SWI-Prolog doesn’t allow non-members to submit issues. Is that by design?

1 Like
2

Hi, you are right, the current implementation of s(CASP) does not allow disunities between two unbound variables at run-time. E.g., the rule:

  p(X,Y) :- X \= Y.

for the query ?- p(1,Y) returns an answer:

{ p(1,Y | {Y \= 1}) }

while the query ?- p(X,Y) does not.
This is a limitation that we plan to address in the future.

3 Likes
3

Thanks so much!

Is there a more elegant work-around than the one I have proposed, letting the user specify the number of objects of each category that should be hypothesized to exist?

And is there a way that I can make my loops appear the same way in the justifications that they appear when using the #abducible p(X). syntax?

4

No. I thought this was enabled by default, but apparently it is not (anymore?). Should be enabled now.

The SWI-Prolog version extends the :- pred rules to match a tree, e.g.,

 :- pred p(X)-[q(Y)]:: "bla {{X} bla {{Y}".

If the left handle of the - matches a node, it will match elements of the children list with the children in the tree, leaving those that do not appear in the pred template. So, called with

 p(a)-[q(b),r(c)]

if will say

bla a bla b holds because
    r(c) holds..

In addition atoms in the tree can have conditions, so you can write

  :- pred (p(X),integer(X)) :: "...".

to make this translation only work for integers. See atom_cond/4 in pr_rules.pl. Should add some docs …

Finally, as the tree is a well defined structure, you can use any Prolog code to rewrite the tree before handing it to the human justification generator.

1 Like
5

Documented inline with atom_cond/4. Copied here:

atom_cond(+Spec, -Atom, -Children, -Condition) is det.

Translate a pred/1 condition. Spec specifies a node in the justification tree. Its general form is AtomSpec-Children, where Children is one of

  • A list of specifications. The specification matches if each specification in the children list matches one of the children of the justification tree. Non-matched children remain in the tree and are used as justification normally. If the list ends with -, e.g. [p(X)|-], all non-matched children are discarded.
  • The atom -. All children are discarded.
  • The atom *. This is the default if there are no children and causes the node to be processed normally.

Each AtomSpec is either a plain Atom, one wrapped, -(Atom) not(Atom) or not(-(Atom)). A condition may be added to an Atom as a conjunction, e.g., this denotes the atom p(X), but only if X
is an integer.

   :- pred (p(X),integer(X)) :: "bla bla {{X}}".
2 Likes
6

That is all very helpful, thanks, @Jan. I find that you guys are adding features to the library faster than I can possibly keep up with them, but I’ve added that one to the backlog.

To re-iterate my last remaining question,

Elegance is subjective, but I’d be interested in any thoughts.

7

We ran in a similar problem (if I understand you correct). The solution we went for is have a helper that returns a number if some object is in a category and a final rules that says that the sum of these numbers should have some value (or value range). So, you have something like this (forgot the details).

select :-
     type_1(Score1),
     type_2(Score2),
     ...
     Score == 5.

type1(1) :- type1.
type1(0).
...