/* declaring operators with precedence classes. precedence used is as follows:
 ~(not) higher than /\ (and).
 /\ higher than \/ (or).
 \/ higher than -> (implication).
*/

:- op(400, xfx, /\) .
:- op(800, xfx, nand) .
:- op(500, xfx, \/).
:- op(900, xfx, xor).
:- op(600, xfx, ->).
:- op(700, xfx, <->).
:- op(300, fx, ~).

/* the rules for the logical operators.
   basic principle is that they evaluate to true if the eval of their
   arguments evaluate to true within certain conditions.

   /\ evaluates to true if both its arguments are true.
   /\ evaluates to true if either or both its arguments evaluate to true.
   ~ evaluates to true if its argument evaluates to false (and vice versa)
   => evaluates to true if both its arguments evaluate to true, or its first
      argument evaluates to false.

   the eval functions catch each logical operator and combine the result
   of evaluating its arguments to match the structure of the operator.

   the eval(X) is the base case that checks that X is an atom and that it is tru
e.
*/

eval(X) :- atom(X), true(X).
eval(~X) :- \+ eval(X).
eval(X /\ Y) :- eval(X), eval(Y).
eval(X \/ Y) :- eval(X).
eval(X \/ _) :- eval(Y).
eval(_ \/ Y) :- eval(X), eval(Y).
eval(X xor Y) :- eval(X), \+ eval(Y).
eval(X xor Y) :- eval(Y), \+ eval(X).
eval(X -> _) :- \+ eval(X).
eval(X -> Y) :- eval(X), eval(Y).
eval(X <-> Y) :- \+ eval(X), \+ eval(Y).
eval(X <-> Y) :- eval(X), eval(Y).
eval(X nand Y) :- \+ eval(X /\ Y).

/* any atoms that are to be true within the formula provided are declared as
   true here
*/
true(p).

latom(X) :- atom(X).
latom(~ X) :- atom(X).

/* operator elimination */
elim(X, Z) :- latom(X), Z = (X).
elim(~ X, Z) :- elim(X, P), Z = (~ (P)).
elim(X /\ Y, Z) :- elim(X, P), elim(Y, Q), Z = ((P) /\ (Q)).
elim(X \/ Y, Z) :- elim(X, P), elim(Y, Q), Z = ((P) \/ (Q)).
elim(X -> Y, Z) :- elim(X, P), elim(Y, Q), Z = (~(P) \/ (Q)).
elim(X <-> Y, Z) :- elim(X, P), elim(Y, Q), Z = (((P) /\ (Q)) \/ (~(Q) /\ ~(P)))
.
elim(X nand Y, Z) :- elim(X, P), elim(Y, Q), Z = (~ ((P) /\ (Q))).
elim(X xor Y, Z) :- elim(X, P), elim(Y, Q), elim((P <-> Q), R), Z = (~(R)) .

elimWrite(X) :- elim(X, Z), write(Z).

/* negative normal form */
nnf(X, Z) :- latom(X), Z = (X).
nnf(~ (~ (X)), Z) :- nnf(X, P), Z = P.
nnf(~ (X \/ Y), Z) :- nnf(~ X, P), nnf(~ Y, Q), Z = ((P) /\ (Q)).
nnf(X /\ Y, Z) :- nnf(X, P), nnf(Y, Q), Z = ((P) /\ (Q)).
nnf(X \/ Y, Z) :- nnf(X, P), nnf(Y, Q), Z = ((P) \/ (Q)).
nnf(~ (X /\ Y), Z) :- nnf(~ X, P), nnf(~ Y, Q), Z = ((P) \/ (Q)).

nnfWrite(X) :- nnf(X, Z), write(Z).

/* conjuctive normal form */

cnf(X, Z) :- latom(X), Z = (X).
cnf(X /\ Y, Z) :- cnf(X, P), cnf(Y, Q), Z = ((P) /\ (Q)).
cnf((X /\ Y) \/ W, Z) :- cnf(X, P), cnf(Y, Q), cnf(W, R), Z = (((P) \/ (R)) /\ (
(Q) \/ (R))).
cnf(W \/ (X /\ Y), Z) :- cnf(W, R), cnf(X, P), cnf(Y, Q), Z = ((P) \/ (R)) /\ ((
Q) \/ (R)).
cnf(X \/ Y, Z) :- cnf(X, P), latom(Y), Z = ((P) \/ (Y)).
cnf(X \/ Y, Z) :- latom(X), cnf(Y, P), Z = ((X) \/ (P)).

cnfWrite(X) :- cnf(X, Z), write(Z).