% problem-set/algebra/rings/Stickel.p.clauses % created : 07/11/86 % revised : 07/13/88 % description : % % The following clauses are given by Stickel as a complete set % of reductions for ring theory. % representation : % % declare_predicates(3,[S,P]). % declare_functions(2,[j,f]). % declare_function(1,g). % declare_constants([0]). % declare_variables([x,y,z,v1,v2,v3,v4]). % % S means sum, P means produce; j(x,y) is the sum of x and y, f(x,y) % is the product of x and y; g(x) is the additive inverse of x; % 0 is the additive identity element % Left identity S(0,x,x). % Left inverse S(g(x),x,0). % Distributivity of product over sum -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -P(x,v3,v4) | S(v1,v2,v4). -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(x,v3,v4). -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -P(v3,x,v4) | S(v1,v2,v4). -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(v3,x,v4). % inverse of 0 is 0 S(g(0),0,0). % inverse of inverse of x is x S(g(g(x)),0,x). % behavior of 0 and multiplication P(x,0,0). P(0,x,0). % inverse of (x + y) = inverse(x) + inverse(y) S(g(x),g(y),g(j(x,y))). % x * inverse(y) = inverse (x * y) P(x,g(y),g(f(x,y))).