When it got pointed out that it wasn't the first but the subsequent call to validate that failed I could trace it to a misspelling of the word 'assumption'.
Why does this not unify? (Prolog)
-
04-07-2022 - |
Question
I'm writing a proof-checker for natural deduction, and I'm having a problem with parts of the proof that go "one step further" down the list.
First I read a file etc, and then I call the function that is causing trouble:
validate([q],[[1, q, premise],[[2, p, assumption],[3, q, copy(1)]],
[4, imp(p,q), impint(2,3)]].
From checking with trace I know that the call below is the one that fails:
validate([[1, q, premise], q], [[[2, p, assumption], [3, q, copy(1)]], [4, imp(p, q), impint(2, 3)]])
These are the relevant parts of the program:
%% 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).
Solution
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow