Abstracts of Technical Reports Computer Science Branch, Corporate Research and Development, General Electric Company, Schenectady, NY 12345 (GE)
Franz Winkler · ACM SIGSAM Bulletin · 1987
The unification problem for terms containing associative and commutative functions is of great importance in theorem provers based on the rewriting approach and resolution methods. The complexity of checking whether two such terms are unifiable was known to be NP-hard. It is proved that the problem is NP-complete by describing a nondeterministic polynomial time algorithm for it. It is also shown that if in addition, an associative-commutative function is assumed to be idempotent and/or have an identity, the problem still remains NP-complete.