@inproceedings{e75ab5906c5440d38919323242639917,
title = "Double-exponential complexity of computing a complete set of AC-unifiers",
abstract = "An algorithm for computing a complete set of unifiers for two terms involving associative-commutative function symbols is presented. It is based on a nondeterministic algorithm given by the authors in 1986 to show the NP-completeness of associative-commutative unifiability. The algorithm is easy to understand, and its termination can be easily established. Its complexity is easily analyzed and 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.",
author = "Deepak Kapur and Paliath Narendran",
year = "1992",
month = jun,
language = "English",
isbn = "0818627352",
series = "Proceedings - Symposium on Logic in Computer Science",
publisher = "Publ by IEEE",
pages = "11--21",
booktitle = "Proceedings - Symposium on Logic in Computer Science",
note = "Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science ; Conference date: 22-06-1992 Through 25-06-1992",
}