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). 
Was it helpful?

Solution

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'.

Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top