Many thanks Jan for your help. I suspected that I was in a dead end, and I remember now that you told me that I needed subst/4. Sorry to be so slow.
I publish here the file variable-boole-quine-pl that provide a clear pretty-printing reflecting the work of the prover, here is the last version of this file:
/*
This prover is the work of Jan Burse. I changed only the symbols for operators, that's it.
See the web page : https://swi-prolog.discourse.group/t/implementing-quines-algorithm/2830
and also https://stackoverflow.com/questions/63505466/prolog-implementation-of-quines-algorithm-for-classical-propositional-logic-in?noredirect=1#comment112667699_63505466
the boole.pl original file is here: https://gist.github.com/jburse/4ab909be4406b0c960494c692fc7a37f#file-boole-pl
*/
:- use_module(library(statistics)).
:- op(700, xfy, <=>).
:- op(600, xfy, =>).
:- op(500, xfy, v).
:- op(400, xfy, &).
:- op(300, fy, ~).
eval(A, A) :- var(A), !.
eval(A => B, R) :- !, eval(A, X), eval(B, Y), simp(X => Y, R).
eval(A <=> B, R) :- !, eval(A, X), eval(B, Y), simp(X <=> Y, R).
eval(A v B, R) :- !, eval(A, X), eval(B, Y), simp(X v Y, R).
eval(A & B, R) :- !, eval(A, X), eval(B, Y), simp(X & Y, R).
eval(~A, R) :- !, eval(A, X), simp(~X, R).
eval(A, A).
simp(A, A) :- var(A), !.
simp(A => _, 1) :- A == 0, !.
simp(A => B, X) :- B == 0, !, simp(~A, X).
simp(A => B, B) :- A == 1, !.
simp(_ => B, 1) :- B == 1, !.
simp(A <=> B, X) :- A == 0, !, simp(~B, X).
simp(A <=> B, X) :- B == 0, !, simp(~A, X).
simp(A <=> B, B) :- A == 1, !.
simp(A <=> B, A) :- B == 1, !.
simp(A v B, B) :- A == 0, !.
simp(A v B, A) :- B == 0, !.
simp(A v _, 1) :- A == 1, !.
simp(_ v B, 1) :- B == 1, !.
simp(A & _, 0) :- A == 0, !.
simp(_ & B, 0) :- B == 0, !.
simp(A & B, B) :- A == 1, !.
simp(A & B, A) :- B == 1, !.
simp(~A, 1) :- A == 0, !.
simp(~A, 0) :- A == 1, !.
simp(A, A).
judge(A, [B|R]) :-
eval(A, B),
term_variables(B, L),
judge(B, L, R).
% Boole prover : boole/2
% First, write "boole" + Enter.
% Second, write your formula + Enter.
judge(_, [], R) :- !, R = [].
judge(A, [B|L], R) :-
copy_term(A-[B|L], C-[0|L]),
copy_term(A-[B|L], D-[1|L]),
judge(C & D, R).
boole :-
get_wff(_A,_L).
get_wff(A,L) :-
read_term(A, [variable_names(_N)]),
time(judge(A,L)),
last(L,R),
(
last(L,1) -> write('to prove that the formula is a tautology, i.e. that its truth value is always '),
write(R),write(' .'),nl,nl,nl,
boole
;
last(L,0) -> write('to prove that the formula is not a tautology, i.e. that its truth value can be '),
write(R),write(' .'),nl,nl,nl,
boole
).
/*
Examples:
?- true.
?- boole.
|: A => A.
% 22 inferences, 0.000 CPU in 0.000 seconds (89% CPU, 758202 Lips)
to prove that the formula is a tautology, i.e. that its truth value is always 1 .
|: A => B.
% 30 inferences, 0.000 CPU in 0.000 seconds (93% CPU, 623662 Lips)
to prove that the formula is not a tautology, i.e. that its truth value can be 0 .
|: halt.
% 3 inferences, 0.000 CPU in 0.000 seconds (90% CPU, 53834 Lips)
false.
?-
*/
/*
falsify(A) :- eval(A, B), term_variables(B, L), falsify(B, L).
falsify(0,_) :- !.
falsify(A, [0|_]) :- falsify(A), !.
falsify(A, [1|_]) :- falsify(A).
*/
taut(A, T, N) :-
eval(A, B),
write_term(A, [variable_names(N)]),nl,
write_term(B, [variable_names(N)]),nl,
write('------------------------------'),nl,
term_variables(B, L), taut(B, L, T, N),nl.
taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 0, write(N),nl, taut(A, T, N), throw(T)), T, true),
B = 1, write(N),nl, taut(A, S, N), T = S.
% Second prover, more practical and more verbose:
% First, write "quine" + Enter.
% Second, write only your formula + Enter.
quine:-
getFormula(_A,_T).
getFormula(A, T) :-
read_term(A, [variable_names(N)]),
(time(taut(A, T, N)) -> /* here is the missing outer if-then-else */
(T == 1 ->
write('to prove that the formula is a tautology.'),
nl,nl,nl,
quine
;
write('to prove that the formula is an antilogy.'),
nl,nl,nl,
quine
)
;
write('to prove that the formula is neither a tautology nor an antilogy.'),
nl,nl,nl,
quine
).
/*
Examples:
?- quine.
|: A => A.
A=>A
A=>A
------------------------------
0=>0
1
------------------------------
1=>1
1
------------------------------
% 45 inferences, 0.000 CPU in 0.000 seconds (98% CPU, 158510 Lips)
to prove that the formula is a tautology.
true.
?- quine.
|: A => B.
A=>B
A=>B
------------------------------
0=>B
1
------------------------------
1=>B
B
------------------------------
0
0
------------------------------
1
1
------------------------------
% 73 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 187048 Lips)
to prove that the formula is neither a tautology nor an antilogy.
true.
*/
Example of output with quine prover:
?- quine.
|: A => A.
A=>A
A=>A
------------------------------
[A=0]
0=>0
1
------------------------------
[A=1]
1=>1
1
------------------------------
% 53 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 509361 Lips)
to prove that the formula is a tautology.
|: ((A v B) => C) <=> ((A => C) & (B => C)).
A v B=>C<=>(A=>C)&(B=>C)
A v B=>C<=>(A=>C)&(B=>C)
------------------------------
[A=0,B=_4768,C=_4774]
0 v B=>C<=>(0=>C)&(B=>C)
B=>C<=>B=>C
------------------------------
[A=0,B=0,C=_4774]
0=>C<=>0=>C
1
------------------------------
[A=0,B=1,C=_4774]
1=>C<=>1=>C
C<=>C
------------------------------
[A=0,B=1,C=0]
0<=>0
1
------------------------------
[A=0,B=1,C=1]
1<=>1
1
------------------------------
[A=1,B=_4768,C=_4774]
1 v B=>C<=>(1=>C)&(B=>C)
C<=>C&(B=>C)
------------------------------
[A=1,B=_4768,C=0]
0<=>0&(B=>0)
1
------------------------------
[A=1,B=_4768,C=1]
1<=>1&(B=>1)
1
------------------------------
% 241 inferences, 0.001 CPU in 0.001 seconds (99% CPU, 303785 Lips)
to prove that the formula is a tautology.