% Problem: Generalized Near-domains
% Status:  Open Problem
%
% A (right) near-domain (R,+,*,0,1) is a generalization of a (right)
% near-field: (R,+,0) is a (right) Bruck loop, (R\{0},*,1) is a group,
% * distributes over + on the right, and there is another compatibility
% condition (see below) which relates * to the nonassociativity of +. 
% 
% Near-domains are equivalent to sharply 2-transitive groups, in the
% sense that the affine group of any near-domain is a sharply 2-transitive
% group, and any sharply 2-transitive group is the affine group of a
% near-domain. 
%
% The main open problem here: is every near-domain is a near-field,
% that is, is loop (R,+,0) necessarily an abelian group?  In group theory
% language, this is equivalent to: does every sharply 2-transitive group
% have a regular normal subgroup? In that formulation, Zassenhaus (1934)
% proved that the answer is yes in the finite case. Some other special
% cases are known as well.
% 
% For automated theorem proving, the difficulty here is the same as for
% fields: the condition that nonzero elements have multiplicative inverses
% is non-Horn. The formulation below is an attempt to get around this,
% modeled on the Near-ring and Inverse Semigroups Challenge Problem. 
% 
% The idea is to get a purely equational formulation by replacing 
% near-domains with subdirect products of near-domains. So instead of 
% requiring that (R\{0},*,1) is a group, we instead require that (R,*,1)
% is an inverse semigroup. For lack of a better term, call that structure
% a generalized near-domains. The new problem here in high-level language:
%
% Is every generalized near-domain a subdirect product of near-fields?
%
% More simply: in a generalized near-domain, is (R,+,0) an abelian group?
% An affirmative answer would immediately imply a positive solution to the
% original problem. 
%
% The goal below is commutativity of +. This is known to imply 
% associativity of +.
%
% As usual, the formulation is not minimal. Various axioms which are 
% consequences of others are included in case they might help. For 
% instance, the long commented-out axiom for + (which might clog the
% search) is a consequence of the rest.

formulas(assumptions).

% (R,+,0) is a right Bruck loop.
0 + x = x. x + 0 = x.
x + -x = 0. -(-x) = x.
(y + x) + -x = y.
-(x + y) = (-x) + (-y).
((z + x) + y) + x = z + ((x + y) + x).
(y + x) + (y + x) = (x + (y + y)) + x.
%(((x + y) + z) + -(y + z)) + (((u + y) + z) + -(y + z)) =
%(((x + u) + y) + z) + -(y + z).

% (R,*,1) is an inverse (hence Clifford) semigroup
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'. 1' = 1. 0' = 0.
(x * x') * y = y * (x * x').

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

% key compatibility condition
(z * (((1 + y) + x) + -(y + x))) + (y + x) = (z + y) + x.

end_of_list.

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