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.