% 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))).