% problem-set/algebra/boolean/prob4_part1.ver2 % created: 08/08/89 % revised: 08/08/89 % description: % % This problem is designed to prove that x * (x + y) = x in boolean % algebra. % This version uses equality representation and demodulators. % Paramodulation is the inference rule. % 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]). set(dynamic_demod). set(para_from). set(para_into). set(para_from_right). set(para_from_left). assign(max_seconds,40). 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). % 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 -(prod(a,sum(a,b)) = a). 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))). % 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.