Hello.
I would be glad to publish the prover below online, to be used online on my website. The simplest way would be the best, but I need clear and complete explanations. Thanks !
/*
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
% 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
).
% Second prover, Quine prover more practical and more verbose:
% First, write "quine" + Enter.
% Second, write only your formula + Enter.
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,taut(A, T, N), throw(T)), T, true),
B = 1, write(N),nl,nl,taut(A, S, N), T = S.
*/
taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 1,write(N),write(':'),nl,nl,taut(A, T, N),throw(T)), T, true),
B = 0,
write(N),write(':'),nl,nl,
taut(A, S, N), T = S.
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
).