为什么不统一呢？（序言）答案

【问题标题】：Why does this not unify? (Prolog)为什么不统一呢？（序言）
【发布时间】：2013-11-06 19:59:14
【问题描述】：

我正在为自然演绎编写一个证明检查器，但我在证明中“更进一步”的部分存在问题。

首先我读取一个文件等，然后调用导致问题的函数：

validate([q],[[1, q, premise],[[2, p, assumption],[3, q, copy(1)]], 
[4, imp(p,q), impint(2,3)]].

通过跟踪检查，我知道下面的调用是失败的：

validate([[1, q, premise], q], [[[2, p, assumption], [3, q, copy(1)]], [4, imp(p, q), impint(2, 3)]])

这些是程序的相关部分：

%% Premise, this is what should unify at the first call %%
validate(Prems,[[N,Y,premise]|T]):-
   member(Y,Prems),
   validate([[N,Y,premise]|Prems],T).

%% This is not being called at the moment, so feel free to ignore it, since it's the next step.%%
%%Box, or the deeper level. This should be called from the sentance above%%
validate(Prems, [[[N,X,assumtion]|BT]|Tail]):-
  reverse([[[N,X,assumtion]|BT]|Tail], RevBox),
  RevBox = [[M,Goal,X]|_], 
  write('1'),
  validate([[N,X,assumtion]|Prems],BT),
  write('2'),
  validate([[X,Goal, box(N,M)]|Tail]).

%%impint%%
validate(Prems, [[N,imp(P,Q),impint(A,B)]|T]):-
 member([P,Q,box(A,B)],Prems),
 write('3'),
 validate([[N,imp(P,Q),impint(A,B)]|Prems],T).

%% copy %%
validate(Prems,[[_,X,copy(A)]|T]):-
 member([A,X,_],Prems),
 validate([[_,X,copy(A)]|Prems],T).

【问题讨论】：

有时它的 validate/1 有时 validate/2。我认为你必须展示整个程序。你问为什么不；这[...] 与validate(_,_) 统一。什么意思？
您是否尝试运行trace？并不是说它没有匹配一个子句开始。它在第一次递归调用时无法匹配。
@false 我添加了可能被调用的代码，并修复了最后一行。
@mbratch 是的，我做到了，我看到问题顶部的调用是失败的调用。我希望它/认为它应该匹配 validate(Prems,[[N,Y,premature]|T])，但它不匹配。
它确实符合那个条款。随后的递归调用不匹配。

标签： prolog unification

【解决方案1】：

当它被指出不是第一次而是随后的验证失败时，我可以将其追溯到单词“假设”的拼写错误。

【讨论】：