Is there a name for the generalization of the concept "Abelian group" where the axiom $-x+x = 0$ is weakened to the following?

Question

Is there a name for the generalization of the concept "Abelian group" where the axiom $−x+x=0$ is replaced by the following list?

1. $−0=0$
2. $−(x+y)=−x+−y$
3. $−(−x)=x$
4. $x+(-x)+x = x$

In multiplicative notation; we replace the axiom $x^{-1}x=1$ with the following list:

1. $1^{-1}=1$
2. $(xy)^{-1}=x^{-1}y^{-1}$
3. $(x^{-1})^{-1}=x$
4. $xx^{-1}x = x$

Examples.

• Any Abelian group satisfies the above axioms in their additive form.
• The multiplicative structure of any zero-totalized field satisfies the above axioms in their multiplicative form, but does not satisfy $x^{-1}x=1$, since $0^{-1} \cdot 0 = 0 \cdot 0 = 0$.

Answer 1

Apparently it's called a (commutative) inverse monoid. For further details, see Wikipedia^{1, 2, 3} or Lawson's Inverse Semigroups⁴.

(I haven't proven that the sets of axioms are equivalent. You may want to reserve the bounty for someone who does so.)