Abstract of Paper

AC(U)ID-Unification is NEXPTIME-Decidable
by Siva Anantharaman, Paliath Narendran and Michael Rusinowitch

Abstract:

We consider the unification problem for the equational theory 
AC(U)ID obtained  by adjoining a binary symbol `*' which is 2-sided 
distributive over an associative-commutative idempotent operator `+'. 
We formulate the problem as a particular class of set constraints, 
and propose a method for solving it by using the dag automata 
introduced by W. Charatonik, which are  enriched with labels for 
our purposes. AC(U)ID-unification is thus shown to be in NEXPTIME.