Many-sorted unification

47Citations
Citations of this article
15Readers
Mendeley users who have this article in their library.

Abstract

Many-sorted unification is considered; that is, unification in the many-sorted free algebras of terms, where variables, as well as the domains and ranges of functions, are restricted to certain subsets of the universe, given as a potentially infinite hierarchy of sorts. It is shown that complete and minimal sets of unifiers may not always exist for many-sorted unification. Conditions for sort hierarchies that are equivalent for the existence of these sets with one, finitely many, or infinitely many elements are presented. It is also proved that being a forest-structured sort hierarchy is a necessary and sufficient criterion for the Robinson Unification Theorem to hold for many-sorted unification. An algorithm for many-sorted unification is given. © 1988, ACM. All rights reserved.

Cite

CITATION STYLE

APA

Walther, C. (1988). Many-sorted unification. Journal of the ACM (JACM), 35(1), 1–17. https://doi.org/10.1145/42267.45071

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free