We consider equational unification and matching problems where the equational theory contains a nilpotent function, i.e., a function f satisfying f(x,x) = 0 where 0 is a constant. Nilpotent matching and unifiction are shown to be NP-complete. In the presence of associativity and commutativity, the problems still remain NP-complete. But when 0 is also assumed to be the unity for the function f, the problems are solvable in polynomial time. We also show that the problem remains in P even when a homomorphism is added. Secon-order matching modulo nilpotence is shown to be undecidable.
展开▼
