:- expects_dialect(lps).

% Code given by Jan Burse alias "Mostowski Collapse" here:
% https://stackoverflow.com/questions/63505466/prolog-implementation-of-quines-algorithm-for-classical-propositional-logic-in
% It was very easy to complete the code to get a full translation of Quine's algorithm.
% Operators first 
:- op(700, xfy, <=>).
:- op(600, xfy, =>).
:- op(500, xfy, v).
:- op(400, xfy, &).
:- op(300, fy, ~).
% Code to get the *recursive* evaluation of formulas. 
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 & 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, R) :- !, eval(A, X), simp(~X, R).
eval(A, A).
% Quine reduction rules
simp(A, A) :- var(A), !.
simp(A <=> B, B) :- A == 1, !.
simp(A <=> B, A) :- B == 1, !.
simp(A <=> B, ~ B) :- A == 0, !.
simp(A <=> B, ~ A) :- B == 0, !.
simp(A => _, 1) :- A == 0, !.
simp(A => B, B) :- A == 1, !.
simp(_ => B, 1) :- B == 1, !.
simp(A => B, ~ A) :- B == 0, !.
simp(A & _, 0) :- A == 0, !.
simp(_ & B, 0) :- B == 0, !.
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, 1) :- A == 0, !.
simp(~ A, 0) :- A == 1, !.
simp(A, A).
% the prover engine: if A is a tautology, then unsat(A) is false (CLP(B) unsat(F) :- sat(~ F),
% otherwise the values that satisfy unsat(F) (i.e. ~ F) are given).
unsat(A) :- eval(A, B), term_variables(B, L), unsat(B, L).
unsat(0, _) :- !.
unsat(A, [0|_]) :- unsat(A), !.
unsat(A, [1|_]) :- unsat(A).



/*
Examples: 

?- unsat(~ ~ A <=> A).
false.

?- unsat(A => B).
A = 1,
B = 0.

*/