我正在为自然推论编写一个证明检查器，但我对在列表中“更进一步”的部分证明存在问题。
首先我读取一个文件等，然后调用导致问题的函数：
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).