list - 在Prolog中设置两个兼容列表的差异

Question

我目前正在尝试在 prolog 中实现自动定理证明器，并且偶然发现了一个问题。

如果我有一个列表列表，例如:

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

我如何获得两个兼容列表项的“设置差异”: 我所说的兼容是指，如果某个数字的否定存在于另一个列表中，则用设置的差值替换这两个列表，即: [1,2] 和 [-1,3] 是兼容的，因为 -1 出现在第二个子句中，因此它应该返回设置 [2,3] 的差异，新列表应为 [[2,3],[4,5,7],[-2,4]] .

目前我有以下step谓词:

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).

所以它只是检查每个列表并检查变量的否定是否存在以及是否简单地将其写出来。我已经添加了处理负数的代码，因此 X 将匹配 -X，X 是任何整数。

我现在陷入了困境，非常感谢任何帮助。

Answer 1

另一种可能的解决方案:

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)).

一些例子:

?- 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.