2
votes

I'm currently trying to implement an automated theorem prover in prolog and have stumbled across a problem.

If I have a list of lists such as:

[[1,2],[-1,3],[4,5,7],[-2,4]]

How would I get the "set difference" of two compatible list items: What I mean by compatible is, if the negation of a certain number exists in another list, then replace those two lists with the set difference, ie: [1,2] and [-1,3] are compatible because -1 is present in the second clause and thus it should return the set difference of [2,3] and the new list should be [[2,3],[4,5,7],[-2,4]].

Currently I have the following step predicate:

memberlist(X,[[X|_]|_]).
memberlist(X,[[_|T1]|T2]) :-
    memberlist(X,[T1|T2]).
memberlist(X,[[]|T2]) :-
    memberlist(X,T2).

step([]).
step([_|T]) :-
    memberlist(neg X,T),
    write(X),
    nl,
    step(T).
step([_|T]) :-
    step(T).

So it simply checks each list and checks if the negation of a variable exists and if it does simply write it out. I've already added code which deals with negative numbers, so X will match a -X, X being any integer.

I'm quite stuck at this point, and any help would be greatly appreciated.

2
This is cross posted on SWI-Prolog forum. - Guy Coder

2 Answers

2
votes

Another possible solution:

shrink([L1|R1], [L3|R2]) :-
    select(L2, R1, R2),
    difference(L1, L2, L3).
shrink([L1|R1], [L1|S]) :-
    shrink(R1, S).

difference(L1, L2, L3) :-
    select(X, L1, R1),
    compatible(X, Y),
    select(Y, L2, R2),
    union(R1, R2, L3).

compatible(neg(P), P) :- !.
compatible(P, neg(P)).

Some examples:

?- shrink([[1,2], [neg(1),3], [4,5,6], [neg(2),4]], S).
S = [[2, 3], [4, 5, 6], [neg(2), 4]] ;
S = [[1, 4], [neg(1), 3], [4, 5, 6]] ;
false.

?- shrink([[a,neg(b)], [a,b]], S).
S = [[a]] ;
false.

?- shrink([[rainning], [neg(rainning)]], S).
S = [[]] ;
false.

?- shrink([[rainning], [neg(rainning), wet_grass], [neg(wet_grass), green_grass]], S).
S = [[wet_grass], [neg(wet_grass), green_grass]] ;
S = [[rainning], [neg(rainning), green_grass]] ;
false.

?- shrink([[neg(green_grass)], [rainning], [neg(rainning), wet_grass], [neg(wet_grass), green_grass]], A), shrink(A, B), shrink(B, C).

A = [[neg(wet_grass)], [rainning], [neg(rainning), wet_grass]],
B = [[neg(rainning)], [rainning]],
C = [[]] ;

A = [[neg(wet_grass)], [rainning], [neg(rainning), wet_grass]],
B = [[neg(wet_grass)], [wet_grass]],
C = [[]] ;

A = [[neg(green_grass)], [wet_grass], [neg(wet_grass), green_grass]],
B = [[neg(wet_grass)], [wet_grass]],
C = [[]] ;

A = [[neg(green_grass)], [wet_grass], [neg(wet_grass), green_grass]],
B = [[neg(green_grass)], [green_grass]],
C = [[]] ;

A = [[neg(green_grass)], [rainning], [neg(rainning), green_grass]],
B = [[neg(rainning)], [rainning]],
C = [[]] ;

A = [[neg(green_grass)], [rainning], [neg(rainning), green_grass]],
B = [[neg(green_grass)], [green_grass]],
C = [[]] ;
false.
1
votes

An alternative formulation.

  • memberlist will give you the triples p(X, Y, Z) where Z and neg(Z) are in X and Y.
  • collapse will take such a triple and remove X, Y from Xs and add X+Y-Z-neg(Z) to it.
memberlist([X|Xs], p(X, Y, Z)) :-
    member(Z, X), member(Y, Xs), member(neg(Z), Y).
memberlist([X|Xs], p(X, Y, Z)) :-
    member(neg(Z), X), member(Y, Xs), member(Z, Y).
memberlist([_|Xs], A) :-
    memberlist(Xs, A).

collapse(Xs, Ys) :-
    memberlist(Xs, p(A, B, I)), % A and B have some I and neg(I) in them
    select(A, Xs, XsA),         % remove A
    select(B, XsA, XsAB),       % remove B
    append(A, B, AB), select(I, AB, ABI), select(neg(I), ABI, ABII),
    Ys = [ABII|XsAB].

Your example

?- collapse([[1, 2], [neg(1), 3], [4, 5, 7], [neg(2), 4]], X).
X = [[2, 3], [4, 5, 7], [neg(2), 4]] ;
X = [[1, 4], [neg(1), 3], [4, 5, 7]] ;
false.