# Implementing Quine's algorithm

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) :-
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) :-
(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.
``````

In my opinion, the reply should be yes, the four additional rules of G4 are all rules in minimal logic, and therefore must be derivable in any classical sequent system.

Dear Jan. You overestimate me. As you can see, I did not understand this homework.
To reply to your question on G4c, it is neither Dyckhoff’s nor Negri, I wanted only make the minimal adding to prove classical theorems inside a G4 system, i.e. with rule L -> -> only. Ax-c is classical by contrast with Ax of G4i in this prover: it accepts multi-conclusions.

Sorry for the delay of my reply Jan. These formulas are in the seqprover webpage. Naouki Tamura could certainly say more about them.

I add that I have indeed a github webpage, but I have not yet published the php program for G4i, program that is not written by me but by a good friend of mines.

Congrats Jan ! I am always working at the moment on my quine-wang.pl . The square-brackets problem is behind me, but there is still at least one user inconvenience that I would be glad to solve. I will be back soon.

Best,

Jo.

I do not know if there are provers for free logics. That’s an interesting question.

``````
G4 Prover: a Prolog Prover for Roy Dyckhoff's Sequent Calculus G4
This prover is a fork made by Joseph Vidal-Rosset (joseph.vidal-rosset@gmail.com),
from seqprover.pl, the sequent prover for CL-X, written by Naoyuki Tamura (tamura@kobe-u.ac.jp).
Type "help." if you need some help.
fol(g4i)> fol(g4i).
yes
fol(g4i)> output(pretty).
yes
fol(g4i)> _534#(~q(_534))->_534#q(_534)-->_534#q(_534).
Trying to prove with threshold = 0 1 2 3 4 5
Fail to prove _534#(~q(_534))->_534#q(_534) --> _534#q(_534) (232271 msec.)
yes
fol(g4i)> quit.
yes
Exit from Sequent Calculus Prover...
Total CPU time = 232271 msec.
true
``````

Fortunately, imogen confirms that it is correct:

``````joseph@mx:~\$ imogen fol prove -i "(exists X.(~ q(X)) -> exists X.(q(X))) -> exists X.(q(X))"
Unprovable.
joseph@mx:~\$ imogen fol prove -i "~ ~ ((exists X.(~ q(X)) -> exists X.(q(X))) -> exists X.(q(X)))"
Provable.
``````

Your formula is provable, but only in classical FOL. It is proved by g4c as follows:

``````fol(g4c)> _534#(~q(_534))->_534#q(_534)-->_534#q(_534).
Trying to prove with threshold = 0 1 2
Succeed in proving _534#(~q(_534))->_534#q(_534) --> _534#q(_534) (41 msec.)
pretty:1 =
------------------------------------------------------ Ax-c
bot->X#q(X),q(X),X@(~q(X)->X#q(X)) --> bot,q(X),X#q(X)
------------------------------------------------------ R#-c  ----------------------------------- Ax
bot->X#q(X),q(X),X@(~q(X)->X#q(X)) --> bot,X#q(X)          X#q(X),X@(~q(X)->X#q(X)) --> X#q(X)
---------------------------------------------------------------------------------------------- L->->(4)
(q(X)->bot)->X#q(X),X@(~q(X)->X#q(X)) --> X#q(X)
------------------------------------------------ L~def
~q(X)->X#q(X),X@(~q(X)->X#q(X)) --> X#q(X)
------------------------------------------ L@
X@(~q(X)->X#q(X)) --> X#q(X)
---------------------------- L#->
X#(~q(X))->X#q(X) --> X#q(X)
yes
fol(g4c)> quit.
``````

and via Naoyuki CL-X (seqprover.pl):

``````Trying to prove with threshold = 0 1 2

------------------------------ Ax
q(Y) --> X#(~q(X)),q(Y),X#q(X)
------------------------------ R#
q(Y) --> X#(~q(X)),X#q(X)
--------------------------- R~
--> ~q(Y),X#(~q(X)),X#q(X)
--------------------------- R#  ----------------- Ax
--> X#(~q(X)),X#q(X)        X#q(X) --> X#q(X)
---------------------------------------------- L->
X#(~q(X))->X#q(X) --> X#q(X)

``````

To end on this point, I wonder if a logic that would use classical connective but non-classical quantifiers can be fully consistent: after all, exists X.f(X) is a kind of alternation, to speak like Quine.