Abstract
We are interested in first order unification problems and more specifically in the hierarchy of equational theories based on the cardinality of the set of most general unifiers.
The following result is established in this paper: if T is a suitable first-order equational theory that is finitary, then T is not bounded; that is, there is no integer n>l such that for every unification problem < s = t >T, the cardinality of the set of most general unifiers for < s = t >T is at most n. Our interest in this result stems from the description of the unification hierarchy in [Si 64], where it is argued that one of the major open problems of unification theory is to characterize the border between finitary and infinitary theories as well as between unitary and finitary theories. We show that the class of (non-unitary) finitary theories cannot be decomposed into a hierarchy obtained by uniformly bounding the cardinalities of the sets of most general unifiers. Hence, one cannot use the notion of “bounded size” to characterize the difference between finitary and unitary theories.
The National Science Foundation under grant MCS83-/4977.
The “Deutsche Forschungsgemeinschaft“, Sonderforschungsbereich 314, Künstliche Intelligenz, West Germany.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Book, R., Siekmann, J.: “On the Unification Hierarchy”, SEKI Research Report, Universität Kaiserslautern, West Germany, 1955 (full paper submitted)
Fages, F., Huet, G.: “Complete Sets of Unifiers and Matchers in Equational Theories”, Proc. CAAP-83, Springer Lecture Notes in Comp.Sci., vol. 159,1963
Grätzer, G.: “Universal Algebra”, Springer Verlag, 1979
Herold, A., Siekmann, J.: “Unification in Abelian Semigroups”, Univ. Kaiserslautern, 1955
Huet, G.: “Resolution d’equations dans des langages d’ordre 1,2” These d’Etat, Univ. Paris, VII, 1976
Plotkin, G.: ’Building in Equational Theories’, Machine Intelligence, vol. 7,1972
Raulefs, P., Siekmann, J., Szabo, P., Unvericht, F.: “A Short Survey on the State of the Art in Unification Theory”, SIGSAM Bulletin, vol. 13,1979
Siekmann, J.: “Universal Unification”, Proc. of 7th Conf. on Automated Deduction, Springer Lecture Notes on Comp. Sci., vol. 170,1984
Siekmann, J., Szabo, P.: “Universal Unification: A Survey”, Proc. GWAI-62, Springer Fachberichte, vol. 55,1952
Stickel, M.: “A Unification Algorithm for Assoc. Comm. Functions”, JACM. vol.28, no. 3,1981
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Book, R., Siekmann, J.H. (1986). On the Unification Hierarchy. In: Stoyan, H. (eds) GWAI-85. Informatik-Fachberichte, vol 118. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-71145-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-71145-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16451-7
Online ISBN: 978-3-642-71145-9
eBook Packages: Springer Book Archive