% problem-set/algebra/boolean/prob_10.ver1.in % created: 07/09/86 % revised: 07/27/89 % description: % % This problem is designed to prove that -(x + y) = (-x) + (-y). % % This version was taken from: 'Problems and Experiments from and % with Automated Theorem-Proving Programs' - McCharen, Overbeek, and Wos. % Representation: % % 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,b,c,d]). set(hyper_res). assign(max_seconds, 60). list(axioms). % 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)). end_of_list. list(sos). % 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 SUM(a,b,c). SUM(comp(a),comp(b),d). -EQUAL(comp(c),d). end_of_list.