2012/10/11 by Joao Araujo, Michael Kinyon, Araujo, Joao +3
Mathematics · #20M07 #20M18 #FOS: Mathematics #Group Theory (math.GR) #math.GR #msc:20M07 #msc:20M18
paper · pdf · doi:10.48550/arxiv.1210.3285
arxiv created 2012/10/11 · arxiv updated 2012/10/12
An open problem in the theory of inverse semigroups was whether the variety of such semigroups, when viewed as algebras with a binary operation and a unary operation, is 2-based, that is, has a base for its identities consisting of 2 independent axioms. In this note, we announce the affirmative solution to this problem: the identities x(x'x) = x x (x' (y (y' ((z u)' w')'))) = y (y' (x (x' ((w z) u)))) form a base for inverse semigroups where ' turns out to be the natural inverse operation. We recount here the history of the problem including our previous efforts to find a 2-base using automated deduction and the method that finally worked. We describe our efforts to simplify the proof using Prover9, present the simplified proof itself and conclude with some open problems.