Equality of terms containing associative-commutative functions and commutative binding operators is isomorphism complete. (English) Zbl 0708.68021

Automated deduction, Proc. 10th Int. Conf., Kaiserslautern/FRG 1990, Lect. Notes Comput. Sci. 449, 251-260 (1990).
[For the entire collection see Zbl 0925.00070.]
It is proved that deciding if two terms containing otherwise uninterpreted associative, commutative and associative-commutative function symbols and commutative variable-binding operators are equal, is polynomially equivalent to determining if two graphs are isomorphic. Similar problems without variable-binding operators are usually NP- complete.
Reviewer: G.Mints


68Q25 Analysis of algorithms and problem complexity


Zbl 0925.00070