Paper: Double-exponential complexity of computing a complete set of AC-unifiers (at LICS 1992)

Authors: Deepak Kapur Paliath Narendran

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

BibTeX

  @InProceedings{KapurNarendran-Doubleexponentialco,
    author = 	 {Deepak Kapur and Paliath Narendran},
    title = 	 {Double-exponential complexity of computing a complete set of AC-unifiers },
    booktitle =  {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)},
    year =	 {1992},
    month =	 {June}, 
    pages =      {11--21},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }