% Problem:  Near-rings and inverse semigroups
% Status:   Challenge Problem
%
% Theorem: Let (R,+,*) be a (right) near-ring such that
% (R,*) is an inverse semigroup. Then + is commutative.
%
% There is a high-level proof in
%
% S. J. Mahmood, J. D. P. Meldrum and L. O'Carroll,
% Inverse semigroups and near-rings,
% J. London Math. Soc. 23 (1981), 45-60.
%
% They show that the multiplicative semigroup of a near-ring is an
% inverse semigroup if and only if the near-ring is a subdirect product
% of near-fields. The addition in a near-field is well-known to be commutative.
%
% The formulation below is not "minimal". There are some clauses which are
% easy consequences of the rest just to move things along.
%
% Working with right near-fields instead of left near-fields is just a matter
% of taste. The problem seems to be hard in either version.
%
% For using proof sketches, it might be helpful to first find a proof for
% near-fields. However, this will make the problem non-Horn. Here are the
% additional axioms for a near-field: 
% x != 0 -> x * x' = 1.
% x != 0 -> x' * x = 1.
%
%%%%%%%%%%%%%%%%%%%%%%%

formulas(assumptions).

% (R,+,0) is a group
0 + x = x. x + 0 = x.
x + -x = 0. -x + x = 0.
(x + y) + z = x + (y + z).

% (R,*,1) is an inverse (hence, Clifford) monoid
1 * x = x. x * 1 = x.
(x * y) * z = x * (y * z).
x * (x' * x) = x. x'' = x. x * x' = x' * x.
(x * y)' = y' * x'.
(x * x') * y = y * (x * x').

% right distributive law
(y * x) + (z * x) = (y + z) * x.
x * 0 = 0. 0 * x = 0.

end_of_list.

formulas(goals).
x + y = y + x.
end_of_list.
