% problem-set/algebra/boolean/prob3.ver1.clauses % created: 07/09/86 % revised: 07/27/89 % description: % % This problem is designed to prove that x * 0 = 0 in boolean algebra. % This version is from the McCharen paper [Aug 1976]. % representation: % % PROD(a,b,c) means a * b = c. % SUM(a,b,c) means a + b = c. % % declare_predicates(3,[SUM,PROD]). % declare_predicate(2,EQUAL). % declare_functions(2,[f1,f2]). % declare_function(1,comp). % declare_variables([x,y,z,u,v,v1,v2,v3,v4]). % declare_constants([0,1,a]). % commutative property -SUM(x,y,v3) | SUM(y,x,v3). -PROD(x,y,v3) | PROD(y,x,v3). % distributive property -PROD(x,y,v1) | -PROD(x,z,v2) | -SUM(y,z,v3) | -PROD(x,v3,v4) | SUM(v1,v2,v4). -PROD(x,y,v1) | -PROD(x,z,v2) | -SUM(y,z,v3) | -SUM(v1,v2,v4) | PROD(x,v3,v4). -PROD(y,x,v1) | -PROD(z,x,v2) | -SUM(y,z,v3) | -PROD(v3,x,v4) | SUM(v1,v2,v4). -PROD(y,x,v1) | -PROD(z,x,v2) | -SUM(y,z,v3) | -SUM(v1,v2,v4) | PROD(v3,x,v4). -SUM(x,y,v1) | -SUM(x,z,v2) | -PROD(y,z,v3) | -SUM(x,v3,v4) | PROD(v1,v2,v4). -SUM(x,y,v1) | -SUM(x,z,v2) | -PROD(y,z,v3) | -PROD(v1,v2,v4) | SUM(x,v3,v4). -SUM(y,x,v1) | -SUM(z,x,v2) | -PROD(y,z,v3) | -SUM(v3,x,v4) | PROD(v1,v2,v4). -SUM(y,x,v1) | -SUM(z,x,v2) | -PROD(y,z,v3) | -PROD(v1,v2,v4) | SUM(v3,x,v4). % existence of complements SUM(x,comp(x),1). SUM(comp(x),x,1). PROD(x,comp(x),0). PROD(comp(x),x,0). % the above operations are well defined -SUM(x,y,u) | -SUM(x,y,v) | EQUAL(u,v). -PROD(x,y,u) | -PROD(x,y,v) | EQUAL(u,v). % equality axioms EQUAL(x,x). -EQUAL(x,y) | EQUAL(y,x). -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). % equality substitution axioms -EQUAL(x,y) | -SUM(x,v1,v2) | SUM(y,v1,v2). -EQUAL(x,y) | -SUM(v1,x,v2) | SUM(v1,y,v2). -EQUAL(x,y) | -SUM(v1,v2,x) | SUM(v1,v2,y). -EQUAL(x,y) | -PROD(x,v1,v2) | PROD(y,v1,v2). -EQUAL(x,y) | -PROD(v1,x,v2) | PROD(v1,y,v2). -EQUAL(x,y) | -PROD(v1,v2,x) | PROD(v1,v2,y). -EQUAL(x,y) | EQUAL(f1(x,v1),f1(y,v1)). -EQUAL(x,y) | EQUAL(f1(v1,x),f1(v1,y)). -EQUAL(x,y) | EQUAL(f2(x,v1),f2(y,v1)). -EQUAL(x,y) | EQUAL(f2(v1,x),f2(v1,y)). -EQUAL(x,y) | EQUAL(comp(x),comp(y)). % existence of identities SUM(x,0,x). SUM(0,x,x). PROD(x,1,x). PROD(1,x,x). % closure property SUM(x,y,f1(x,y)). PROD(x,y,f2(x,y)). % denial of the theorem -PROD(a,0,0).