% Predicates for simulating logical formula
false:-!,fail.

boolean(true). boolean(false).
boolean(P,Q):-boolean(P),boolean(Q).
boolean(P,Q,R):-boolean(P,Q), boolean(R).
:-op(1000, fx, boolean).
boolean [].
boolean [P|List]:-boolean(P), boolean List.
boolean P:- boolean(P).

% definition of substitutions
:-op(600, xfx, eq).
not true eq false.
not false eq true.
not not P eq P:-nonvar(P).

% definition of implication.
:-op(600,xfx,=>).
false=>true.
false=>false.
true=>true.
P=>Q:-P eq R, R=>Q.
P=>Q:-Q eq R, P=>R.

% definition of logical equivalence
:-op(600,xfx,iff).
true iff true.
false iff false.
P iff Q:-P eq R, R iff Q.
P iff Q:-Q eq R, P iff R.

:-op(600, yfx, and).
true and true.
P and Q:-P eq R, R and Q.
P and Q:-Q eq R, P and R.

:-op(600, yfx, or).
true or false.
false or true.
true or true.
P or Q:-P eq R, R or Q.
P or Q:-Q eq R, P or R.