In Hans-Jürgen Bürckert and Werner Nutt, editors, Extended Abstracts of the Third International Workshop on Unification, SEKI-Report SR-89-17, pages 106-110, Lambrecht, FRG, June 26-28, 1989. Fachbereich Informatik, Universität Kaiserslautern.
Full version: Unification in Order-Sorted Signatures, Forschungsbericht 298, Fachbereich Informatik, Universität Dortmund, 1989. [Dvi file, 38 kB]
Abstract: Unification in an order-sorted signature differs substantially from many-sorted unification. If the signature is finite and regular, unification is finitary, but the size of a minimal complete set of unifiers may grow exponentially with the number of variables in the terms to be unified; besides the unifiability problem is in general NP-complete. We give a decidable necessary and sufficient criterion for unitary unifiability, i.e., for the existence of a most general unifier.