|Title||E-unifiability via Narrowing|
|Authors||Emanuele Viola, Dip. di Scienze dell'Informazione, Univ. di Roma 'La Sapienza'|
|Main Fields||4. computational complexity
15. term rewriting
|Other Main Fields||Unification|
|Abstract + Keywords||We formulate a narrowing-based decision
procedure for E-unifiability.
Termination is obtained requiring a narrowing bound: a bound on the
length of narrowing sequences. We study general conditions under
which the method guarantees that E-unifiability is in NP. The
procedure is also extended to narrowing modulo AC
(associativity and commutativity).
As an application of our method, we prove NP-completeness of
unifiability modulo bisimulation in process algebra with proper
iteration. We also give (new) proofs, under a unified point of view,
of NP-decidability of I, ACI, ACI1-unifiability and of unifiability
in quasi-groups and central groupoids.