Ph.D. thesis: Unification Modulo Associativity and Idempotency
This thesis shows that the unification problem
for the theory of one associative and idempotent binary function symbol
i.e. the problem of solving systems of equations in free idempotent
The same result is established for the AI-matching problem,
where only equations with variable-free right hand sides
The complexity of the unification problem in the theory of one
associative, idempotent and commutative function symbol
is known to be polynomial.
We describe the complexity
of the unification problems for all equational theories
of a binary function symbol
that consist of associativity and idempotency
together with any set of additional
We also describe the complexity
of the matching problems for these theories.
Unification and matching problems are solved for
combinations of these theories as well.
Finally, we consider the problem of solving equations
from another point of view,
namely, solving equations in a fixed finite idempotent semigroup.
We establish almost identical dichotomy results as in the case of
the unification and matching problems.
Ph.D. thesis (submitted August 2003, successfully defended March 2004) - ps-file
Extended abstract - ps-file
F. Baader(TU Dresden): page 1 , page 2 , page 3 (JPG).
M. Hermann(École Polytechnique): 4 pages (PS).
C. Szabo(Eötvös University): 4 pages (PS).
Teze disertační práce (říjen 2001) (in czech only)