我正在尝试一个定理证明程序。但是规则4似乎执行不力。
% delete
del(X, [X | Tail], Tail).
del(X, [Y | Tail], [Y | Tail1]) :-
del(X, Tail, Tail1).
% remove
remove(X, Y, L1, L2) :-
del(X, L1, L3),
del(Y, L3, L2).
% prove
prove(true).
prove([L1 seq L2]) :-
seq(L1, L2),
!.
% Rule 1
seq(L1, L2) :-
member(X, L1),
member(X, L2),
!.
% Rule 4
seq(L1, L2) :-
Z = or(X, Y),
del(Z, L2, L4),
remove(X, Y, L3, L4),
seq(L1, L3).
prove([[p] seq [q]]).
-生成false,这是正确的。prove([[p] seq [q, r]]).
-生成错误的,正确的。但是
prove([[p] seq [q or r]]).
-已超出全局堆栈。然后我认为规则4有问题。任何想法如何解决此问题?非常感谢。
最佳答案
在规则4中,据我所知,
但这意味着L3不一定会在终止方面取得任何进展。
关于error-handling - Prolog程序超出全局堆栈错误,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/25578215/