% problem-set/algebra/boolean/prob1.ver2 % created: 08/04/89 % revised: 08/04/89 % description: % % This problem is designed to prove that addition is associative in boolean % algebra. This version is from the McCharen paper [Aug 1976]. % This version uses equality representation and demodulators. % Also, the lemmas which have been proven of idempotence are added. % representation: % % prod(a,b) = c means a * b = c. % sum(a,b) = c means a + b = c. % % declare_functions(2,[sum, prod]). % declare_function(1,comp). % declare_variables([x,y,z,u,v,v1,v2,v3,v4]). % declare_constants([0,1,a,b,c]). set(dynamic_demod). set(para_from). set(para_into). set(para_from_right). set(para_from_left). assign(max_seconds,60). list(axioms). % reflexivity (x = x). % commutativity (sum(x,y) = sum(y,x)). (prod(x,y) = prod(y,x)). % distributivity (sum(prod(x,y), z) = prod(sum(x,z), sum(y,z))). (sum(x, prod(y,z)) = prod(sum(x,y), sum(x,z))). (prod(sum(x,y), z) = sum(prod(x,z), prod(y,z))). (prod(x, sum(y,z)) = sum(prod(x,y), prod(x,z))). end_of_list. list(sos). % Lemmas of idempotence (sum(x,x) = x). (prod(x,x) = x). % existence of complements (sum(x, comp(x)) = 1). (sum(comp(x), x) = 1). (prod(x, comp(x)) = 0). (prod(comp(x), x) = 0). % existence of identities (sum(x,0) = x). (sum(0,x) = x). (prod(x,1) = x). (prod(1,x) = x). % denial of the theorem -(sum(a,sum(b,c)) = sum(sum(a,b), c)). end_of_list. list(demodulators). % commutativity (sum(x,y) = sum(y,x)). (prod(x,y) = prod(y,x)). % distributivity (sum(prod(x,y), z) = prod(sum(x,z), sum(y,z))). (sum(z, prod(x,y)) = prod(sum(z,x), sum(z,y))). % idempotence (sum(x,x) = x). (prod(x,x) = x). % existence of complements (sum(x, comp(x)) = 1). (sum(comp(x), x) = 1). (prod(x, comp(x)) = 0). (prod(comp(x), x) = 0). % existence of identities (sum(x,0) = x). (sum(0,x) = x). (prod(x,1) = x). (prod(1,x) = x). end_of_list.