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

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, 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 from Otten’s work:

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

But it loops:

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


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