Pattern-matching: query returns 'no' even when base case provided

Question

I have a simple Prolog-program that I need some help debugging. The point is to extend the program by pattern-matching to create a proof checker for propositional logic. The problem I have is that I get no when I expect yes and my 'fix' (providing a base case for valid_proof_aux) still gives me two solutions and I don't know why.

Not sure how to go about debugging Prolog yet, sorry.

%call:
valid_proof([p],p,[[1, p, premise]])

%src:

reverse_it([],Z,Z).

reverse_it([H|T],Z,Acc) :- reverse_it(T,Z,[H|Acc]).


valid_proof(Prems,Goal,Proof):-
    last(Proof, [_, Goal, _]),
    reverse_it(Proof, RevP, []),
    valid_proof_aux(Prems, RevP) .

valid_proof_aux(Prems,
        [[_,Prop,premise] | T]):-
    memberchk(Prop,Prems),
    valid_proof_aux(Prems,T).

%my 'fix'
valid_proof_aux(_, []) :- true .

Does your program, as you have shown it, actually compile without any warnings or errors? If it does not, what are the warning or error you see? (You should never ignore warnings, they almost invariably show that you have a real problem with your code). — user1812457

Unknown Unknown · Accepted Answer · 2015-09-11T13:05:06

You don't really show how to run the program and what exactly you get (you should edit your question with and add this), so this answer is a bit of a guess, but anyway:

You need the base case either way (as you observe yourself), valid_proof_aux/2 would fail when the list becomes empty [] and does not match [[...]|T] anymore.

?- [] = [_|_]. % try to unify an empty list with a non-empty list
false.

What you need to do to get rid of the choice point is to put the list argument as the first argument.

valid_proof_aux([], _).
valid_proof_aux([[_,Prop,premise]|T], Prems) :-
    memberchk(Prop, Prems),
    valid_proof_aux(T, Prems).

Note that you don't need the :- true., this is implicit. Also, avoid leaving any blanks on the two sides of the | in [Head|Tail].

Pattern-matching: query returns 'no' even when base case provided

1 Answers