Double-exponential complexity of computing a complete set of AC-unifiers

Author

Kapur, Deepak ; Narendran, Paliath

Author_Institution

Dept. of Comput. Sci., State Univ. of New York, Albany, NY, USA

fYear

1992

fDate

22-25 Jun 1992

Firstpage

11

Lastpage

21

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

Keywords

computational complexity; AC-unifiers; NP-completeness; associative-commutative function; associative-commutative unification; complexity; double-exponential; nondeterministic algorithm; AC generators; Algorithm design and analysis; Artificial intelligence; Computer science; Database languages; Equations; Functional programming; History; Logic programming; Upper bound;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science, 1992. LICS '92., Proceedings of the Seventh Annual IEEE Symposium on

Conference_Location

Santa Cruz, CA

Print_ISBN

0-8186-2735-2

Type

conf

DOI

10.1109/LICS.1992.185515

Filename

185515