% problem-set/algebra/boolean/prob_10.ver2 % created: 08/04/89 % revised: 08/04/89 % description: % % This problem is designed to prove that -(x+y) = (-x) + (-y) in boolean % algebra. This version is from the McCharen paper [Aug 1976]. % This version uses equality representation and demodulators. % 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,d]). % 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))). % 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,b) = c). (sum(comp(a), comp(b)) = d). -(comp(c) = d).