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

Set difference of two compatible lists in Prolog

我目前正在尝试在 prolog 中实现自动定理证明器,但遇到了一个问题。

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

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

如何获得两个兼容列表项的“设置差异”: 我所说的兼容的意思是,如果另一个列表中存在某个数字的否定,则用设置的差异替换这两个列表,即: [1,2][-1,3] 是兼容的,因为 -1 出现在第二个子句中,因此它应该 return [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 将匹配 -XX 是任何整数。

我在这一点上陷入困​​境,将不胜感激任何帮助。

替代公式。

  • memberlist 会给你三元组 p(X, Y, Z) 其中 Zneg(Z)XY.[=29= 中]
  • collapse 将采取这样的三元组并从 Xs 中删除 XY 并向其添加 X+Y-Z-neg(Z)
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].

你的例子

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

另一种可能的解决方案:

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.