序言程序出全局堆棧錯誤

Question

我正在嘗試一個定理證明程序。但規則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]]). - 生成錯誤，這是正確的。
prove([[p] seq [q, r]]). - 生成錯誤，正確。
但prove([[p] seq [q or r]]). - 超出全局堆棧。然後我認爲規則4有什麼問題。
任何想法如何解決這個問題？非常感謝。

Answer 1

在第4條，盡我可以告訴你

• 集合Z是一個模板，一個或
• 嘗試從L2中刪除該模板，使L4是什麼被留下來的，並且該模板（X和Y）的組件被填充，
• 找到一個L3，從中可以刪除組件或者可以刪除也可以給出L4,
• 然後您嘗試用L3來解決問題，而不是L2的

但是這意味着L3並不一定會在終止方面取得任何進展。