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.