# What Is Currently Known

We shall now summarize and reference what is known so far (by the end of 2015).

## Associativity and Idempotency

The equational theory of associativity and idempotency (AI) for one dyadic function symbol *f*, called *idempotent semigroups* as defined by

demonstrates an interesting case for essential unifiers. It has been studied very early in the history of unification theory as it is a standard data structure in computer science and artificial intelligence called *bands* [40]. It was the first case to prove Gordon Plotkin’s conjecture that there are theories where the minimal set of unifiers *liU* ?* _{E} (Г)* does not always exist, see [2, 30, 69].

However, with respect to the encompassment order c * _{E}* this well-known situation changes completely as this theory is in fact e-finitary. Associativity and idempotency constitute the algebra of idempotent strings and for technical convenience these two axioms can be reformulated into the equivalent theory for strings

where Symb(s) denotes the symbols occurring in s. This encoding is due to [40] and in [77] we showed, that it can be directed into a canonical (i.e. confluent and terminating) conditional rewrite system. Based on this result Hoche and Szabo showed in [39] that:

Proposition 11.5 *The theory of AI is not nullary with respect to essential unifiers.*

Looking at the proof of this theorem one may suspect that this theory is even unitary, however there are AI-unification problems with more than one essential unifiers:

Proposition 11.6 *AI is not unitary with respect to essential unifiers.*

So finally we have the most striking result:

Theorem 11.2 *The theory AI isfinitary with respect to essential unifiers.*