A new algorithm for computing a complete set of unifiers for two terms involving associative-commutative function symbols is presented. The algorithm is based on a non-deterministic algorithm given by the authors in 1986 to show the NP-completeness of associative-commutative unifiability. The algorithm is easy to understand, its termination can be easily established. More importantly, its complexity can be easily analyzed and is shown to be doubly exponential in the size of the input terms. The analysis also shows that there is a double-exponential upper bound on the size of a complete set of unifiers of two input terms. Since there is a family of simple associative-commutative unification problems which have complete sets of unifiers whose size is doubly exponential, the algorithm is optimal in its order of complexity in this sense. This is the first associative-commutative unification algorithm whose complexity has been completely analyzed. The approach can also be used to show a single exponential complexity for computing a complete set of unifiers for terms involving associative-commutative function symbols which also have the identity. Furthermore, for unification in the presence of associative-commutative-indempotent operators we get a doubly exponential bound.
To view the entire paper click here