How to use of upcase_atom/2 to get uppercase letters in an output

Help! Data Structure
#43

Thanks, I am learning. It will be the occasion of seeing how implementing iterative deepening. If I am not mistaken, Otten uses it for his leanseq_v5.pl, that is his prover for 1st order logic.

I add that I just tested your Prolog rule for => elimination in the following format in interative deepening, if I am not mistaken, this code is leanseq_v5.pl from Otten’s work:

prove(G>D,FV,I,J,K,eimpl(G > D, P1, P2)) :-
     select(B,D,D1),
     prove(G>[A|D1],FV,I,J,J1,P1),
     prove(G> [(A=>B)|D1],FV,I,J1,K,P2).

But it loops:

?- provable((((a=>b)&a)=>b),Proof).
iteration:1

:frowning:

#45

No difficulty with this. The difficulty is for me always the Prolog implementation.