Thanks for this code that helps me understand how pretty printer works in Prolog. I am going to test it in the afternoon. I see the line
current_prolog_flag(sys_print_map, N),
that will not work in SWI-Prolog, but I will send to you a report. Thanks.
I removed the line:
current_prolog_flag(sys_print_map, N),
and I got the following output:
?- judge(((P+Q)=<R)=:=((P=<R)*(Q=<R)), L), pretty(L).
ERROR: Arguments are not sufficiently instantiated
ERROR: In:
ERROR: [12] write_term(∀_10776^ ...,[variable_names(_10788)])
ERROR: [11] pretty([... =:= ...,...|...]) at /home/joseph/MEGA/projets/cours_prolog/boole.pl:100
ERROR: [9] <user>
ERROR:
ERROR: Note: some frames are missing due to last-call optimization.
ERROR: Re-run your program in debug mode (:- debug.) to get more detail.
I come back to a previous solution that provide an output that seems to me clear and useful for students. The part of the code in my file variables-boole-quine.pl that provides the printed proof is this one:
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).
taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 0, taut(A, T, N), throw(T)), T, true),
B = 1, taut(A, S, N), T = S.
% Second prover, more practical and more verbose: First write quine + Enter. Second write only your formula + Enter. That's it.
quine:-
getFormula(_A,_T).
getFormula(A, T) :-
read_term(A, [variable_names(N)]),
( taut(A, T, N),
nl,
( T==1
-> write('The formula is a tautology.'),
nl,
quine
; T==0
-> write('The formula is an antilogy.'),
nl,
quine
)
; falsify(A),
nl,
write('The formula is neither a tautology nor an antilogy.'),
nl,
quine
).
Examples of output:
?- quine.
|: ((A v B) => C) <=> ((A => C) & (B => C)).
A v B=>C<=>(A=>C)&(B=>C)
A v B=>C<=>(A=>C)&(B=>C)
---------------------------
0 v B=>C<=>(0=>C)&(B=>C)
B=>C<=>B=>C
---------------------------
0=>C<=>0=>C
1
---------------------------
1=>C<=>1=>C
C<=>C
---------------------------
0<=>0
1
---------------------------
1<=>1
1
---------------------------
1 v B=>C<=>(1=>C)&(B=>C)
C<=>C&(B=>C)
---------------------------
0<=>0&(B=>0)
1
---------------------------
1<=>1&(B=>1)
1
---------------------------
The formula is a tautology.
|: A => (B v C v D).
A=>B v C v D
A=>B v C v D
---------------------------
0=>B v C v D
1
---------------------------
1=>B v C v D
B v C v D
---------------------------
0 v C v D
C v D
---------------------------
0 v D
D
---------------------------
0
0
---------------------------
1
1
---------------------------
The formula is neither a tautology nor an antilogy.
|:
I trust you easily if you want to tell me that falsify(A) is useless.
I add that this last example of output would be still nicer if it would have the form of a table, we would be very near the format of Quine’s proof.
You are absolutely right, and I am really thankful for your kind and very efficient help.
The code that you gave to me as correction runs smoothly. 
Thanks Jan. It is certainly very efficient and it is interesting. But again, it is not clear enough for some students: this sort of truth-table generator does not show the complete construction of the table, for atom up to the main connective via the tables of subformulas. For pedagogical purposes the best work in my opinion has been published here, by my colleague Michael Rieppel. The java script source code is here. I do not doubt that the same thing can be done in Prolog, but I never saw it.
Thanks ! Now boole prover in my file is :
boole :-
get_wff(_A,_L).
get_wff(A,L) :-
read_term(A, [variable_names(N)]),
time(judge(A,L)),
(
last(L,1) -> write('to prove that the formula is a tautology:'),nl,
write(N),nl,
write(L)
;
last(L,0) -> write('to prove that the formula is not a tautology:'),nl,
write(N),nl,
write(L)
).
It provides clear output.
“My” program? It is your program, Jan. I would be very happy to be able to write such a program. Unfortunately, “ce n’est pas demain la veille”. 
I will have a look on sat/1 and labeling/1.
Here is the boole-quine.pl prover in the last corrected version that I can publish.
/*
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).
taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 0, taut(A, T, N), throw(T)), T, true),
B = 1, 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.
*/I must tell you frankly Jan that even if I am really interested by your question, I am afraid to miss time. Feel free to use the file quine-boole.pl that I just published. I plan to pubish another question here, on another webpage about Wang’s algorithm in Prolog. This work has been done and published here by Ben Hudson, and the prover seems to me correct, but it can certainly be still improved by good Prolog programmers:
See now:
Jan, I have a question about ‘plain.pl’. Can a syntactic change of definition of operator affect the performances of this prover?
Jan, I’m much impressed by plain.pl . Here are the stastics with a very big disjunction that is not valid and proved as being such by plain.pl :
% 447 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 3540510 Lips)
A11 = A21, A21 = A31, A31 = A41, A41 = A51, A51 = A12, A12 = A22, A22 = A32, A32 = A42, A42 = A52, A52 = A13, A13 = A23, A23 = A33, A33 = A43, A43 = A53, A53 = A14, A14 = A24, A24 = A34, A34 = A44, A44 = A54, A54 = A15, A15 = A25, A25 = A35, A35 = A45, A45 = A55, A55 = 0
Now the same formula submitted as input to boole-quine.pl , to the prover boole exactly:
% 2,866,876 inferences, 0.812 CPU in 0.813 seconds (100% CPU, 3529019 Lips)
to prove that the formula is not a tautology, i.e. that its truth value can be 0 .
and to the quine prover now:
% 6,277 inferences, 0.027 CPU in 0.047 seconds (59% CPU, 228329 Lips)
to prove that the formula is neither a tautology nor an antilogy.
But you said that in SAT there are no winner… 
But unfortunately, plain.pl does not succeed in giving an output for the big valid formula that your know:
time(falsify(((~ (( ~ A0 + F) * ((~ ( ~ B20 + B0) + A20) * ((~ ( ~ B0 + A1) + A0) * (
(~ ( ~ B1 + A2) + A1) * ((~ ( ~ B2 + A3) + A2) * ((~( ~ B3 + A4) + A3) *
((~ ( ~ B4 + A5) + A4) * (( ~ ( ~ B5 + A6) + A5) * ((~ ( ~ B6 + A7) + A6)
* ((~ ( ~ B7 + A8) + A7) * ((~ ( ~ B8 + A9) + A8) * ((~ ( ~ B9 + A10) +
A9) * ((~ ( ~ B10 + A11) + A10) * ( ( ~ ( ~ B11 + A12) + A11) * ((~ ( ~ B12
+ A13) + A12) * (( ~ ( ~ B13 + A14) + A13) * ((~ ( ~ B14 + A15) + A14)
* ((~ ( ~ B15 + A16) + A15) * (( ~ ( ~ B16 + A17) + A16) * ((~ ( ~ B17 +
A18) + A17) * ((~ ( ~ B18 + A19) + A18) * (~ (~ B19 + A20) + A19))))
)))))))))))))))))) + F) * (~ ((~ ( ~ B19 + A20) + A19)
* ((~ ( ~ B18 + A19) + A18) * ((~ ( ~ B17 + A18) + A17) * ((~ ( ~ B16 +
A17) + A16) * ((~ ( ~ B15 + A16) + A15) * ((~ ( ~ B14 + A15) + A14) * (
(~ ( ~ B13 + A14) + A13) * ((~ ( ~ B12 + A13) + A12) * ((~ ( ~ B11 + A12)
+ A11) * ((~ ( ~ B10 + A11) + A10) * ((~ ( ~ B9 + A10) + A9) * ((~ ( ~ B8
+ A9) + A8) * ((~ + A7) * ((~ ( ~ B6 + A7) + A6) * ((~ (
~ B5 + A6) + A5) * ((~ ( ~ B4 + A5) + A4) * ((~ ( ~ B3 + A4) + A3) * ((
~ ( ~ B2 + A3) + A2) * ((~ ( ~ B1 + A2) + A1) * ((~ ( ~ B0 + A1) + A0) * (
(~ ( ~ B20 + B0) + A20) * ( ~ A0 + F)))))))))))))))))))))) + F))
)).
Proved via boole:
?- boole.
|: (((( A0 => F) & ((( B20 => B0) => A20) & ((( B0 => A1) => A0) & (
(( B1 => A2) => A1) & ((( B2 => A3) => A2) & ((( B3 => A4) => A3) &
((( B4 => A5) => A4) & ((( B5 => A6) => A5) & ((( B6 => A7) => A6)
& ((( B7 => A8) => A7) & ((( B8 => A9) => A8) & ((( B9 => A10) =>
A9) & ((( B10 => A11) => A10) & ( (( B11 => A12) => A11) & ((( B12
=> A13) => A12) & ((( B13 => A14) => A13) & ((( B14 => A15) => A14)
& ((( B15 => A16) => A15) & ((( B16 => A17) => A16) & ((( B17 =>
A18) => A17) & ((( B18 => A19) => A18) & ((B19 => A20) => A19))))
)))))))))))))))))) => F) & (((( B19 => A20) => A19)
& ((( B18 => A19) => A18) & ((( B17 => A18) => A17) & ((( B16 =>
A17) => A16) & ((( B15 => A16) => A15) & ((( B14 => A15) => A14) & (
(( B13 => A14) => A13) & ((( B12 => A13) => A12) & ((( B11 => A12)
=> A11) & ((( B10 => A11) => A10) & ((( B9 => A10) => A9) & ((( B8
=> A9) => A8) & ((( B7 => A8) => A7) & ((( B6 => A7) => A6) & (((
B5 => A6) => A5) & ((( B4 => A5) => A4) & ((( B3 => A4) => A3) & ((
( B2 => A3) => A2) & ((( B1 => A2) => A1) & ((( B0 => A1) => A0) & (
(( B20 => B0) => A20) & ( A0 => F)))))))))))))))))))))) => F)).
|: |: |: |: |: |: |: |: |: |: |: |: |: |: |: |:
% 41,645 inferences, 0.032 CPU in 0.032 seconds (100% CPU, 1318876 Lips)
to prove that the formula is a tautology, i.e. that its truth value is always 1
and via quine:
% 34,421 inferences, 0.022 CPU in 0.555 seconds (4% CPU, 1564604 Lips) to prove that the formula is a tautology.
Finally Quine prover is a reasonable option, in my opinion.
Unfortunately, no. My first education was in Philosophy, and in France. I am interested in mathematical logic, but my students are often more afraid than interested by formal arguments.
Do not hesitate to write to Jen :
jeotten @ ifi.uio.no
All his programs are in Prolog and he will be certainly interested to have discussions with you.
Every work in Prolog that is related to theorems provers in first order logic (not necessarily classical) interests me. But I stress on the point that my endeavours are mainly to improve my skills, as far as I can.
I am almost quite certain that it is not. Dyckhoff masterly showed that the keypoint is rule L → . Maybe you know well his famous paper where he defined sequent system LJT that is usually called now G4i. From Naoyuki classical sequent prover, I succeeded to implement G4i. It works pretty well in propositional logic, but meets difficulties in intuitionistic predicate calculus. Any improvements will be welcome. I email to you this paper and this fork.
I did it. The file I just sent to you is G4 in general: g4m, g4i, g4c for respectively, minimal, intuitionistic and classical logic.
Thanks for this interesting point on Prolog interpreter.
@j4n_bur53 . With your code:
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).
taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 0, taut(A, T, N), throw(T)), T, true),
B = 1, 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
).
I wonder what I have to change in order to get the same result in a Quine prover working with atoms and not with Prolog variables. I tried different things with your atom provers based on judge/2, but all my tentatives failed.