/* 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).