(*
Date: 28 Oct 90 13:40:47
From: Paul Abbott <Paul_Abbott@other.wri.com>
Subject: Logical Expressions: BooleanAlgebra
To: mathgroup@yoda.ncsa.uiuc.edu

The following code from Dana Scott will works well with Logical expressions. 
It relies on AlgebraicRules (which in turn uses Groebner bases).  
*)
Format[Rep[x:_,_,_]] := x

Rep[x_, g_, p_] + Rep[y_, g_, p_] ^:= Rep[Mod[x+y /.g, p], g, p]
Rep[x_, g_, p_] + y_              ^:= Rep[Mod[x+y /.g, p], g, p]
Rep[x_, g_, p_] * Rep[y_, g_, p_] ^:= Rep[Mod[x*y /.g, p], g, p]
Rep[x_, g_, p_] * y_              ^:= Rep[Mod[x*y /.g, p], g, p]
Rep[x_, g_, p_] ^ y_              ^:= Rep[Mod[x^y /.g, p], g, p]
	

(* Rules for Boolean algebra *)

gbool = 
AlgebraicRules[{p^2 == p,q^2 == q,r^2 == r,s^2 == s,
													t^2 == t,u^2 == u,v^2 == v,w^2 == w},
																					  {w,v,u,t,s,r,q,p}];

e  = Rep[1,gbool,2];																		
 
(* The logical functions *)

and[x_,y_] := e x y;
or[x_,y_]  := e x + y + x y;
imp[x_,y_] := e + x + x y;
iff[x_,y_] := e + x + y;	

(* Examples *)

p ~imp~ q ~imp~ q ~iff~ (p ~or~ q)

(* Mathematica  verifies that "p implies q all implies q"  is equivalent to the
inclusive disjunction of p and q.  This is done by translating everything into
Boolean polynomials and this reduces to 1.  *)

(* An example of an invalid formula *)

p ~iff~ (p ~or~ q) ~iff~ (p ~and~ q)

(* No matter what truth value we give to p, this formula is false.  *)


