|Abstract of Paper|
AC(U)ID-Unification is NEXPTIME-Decidable
by Siva Anantharaman, Paliath Narendran and Michael Rusinowitch
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.