Abstract
Many-sorted unification is considered, i.e. 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. Many-sorted unification is the same as solving an equation in the corresponding heterogeneous ‘order-sorted’ algebra /7/ rather than in a homogeneous algebra. It is proved that many-sorted unification can be classified completely by conditions imposed on the structure of the sort hierarchy. It is shown that complete and minimal sets of unifiers may not always exist for many-sorted unification. Conditions for sort hierarchies which are equivalent to 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, i.e. a criterion for the existence of a most general unifier without ‘auxiliary variables’. An algorithm for many-sorted unification is given. This paper generalizes and extends the results presented in /22/. It is a shortened version of the technical report /24/, to which the reader is referred for any omitted proofs.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
BIRKHOFF, G. Lattice Theory. American Mathematical Society Colloquium Publications, vol xxv, 1967.
COHN, P.M. Universal Algebra. Reidel, Dordrecht, 1981.
CUNNINGHAM, R.J. and DICK, A.J.J. Rewrite systems on a lattice of types. Acta Informatica 22, 2 (1985), pp. 149–169.
EDER, E. Properties of substitutions and unifications. J. Symbolic Computation 1, 1 (1985), pp. 31–46.
FAGES, F. and HUET, D. Complete sets of unifiers and matchers in equational theories. In Proceedings Eight CAAP, Lecture Notes in Computer Science 159 (L'Aquila 1983), pp. 205–220.
FRISCH, A.M. An investigation into inference with restricted quantification and a taxonomic representation. SIGART Newsletter 91 (1985), pp. 28–31.
GOGUEN, J.A., JOUANNAUD, J.-P., and MESEGUER, J. Operational semantics for order-sorted algebra. In Proceedings Twelfth ICALP, Lecture Notes in Computer Science 194 (Nafplion 1985), pp. 221–231.
GOGUEN, J.A., THATCHER, J.W. and WAGNER, E.G. An initial algebra approach to the specification, correctness and implementation of abstract data types. In Current Trends in Programming Methodology 4, R.T. Yeh, Ed., Prentice Hall 1978, pp. 80–321.
HEROLD, A. Some basic notions of first-order unification theory. Interner Bericht 15/83, Universität Karlsruhe, Inst. f. Informatik I (1983), pp. 1–45.
HUET, G. and OPPEN, D.C. Equations and rewrite rules: a survey. In Technical Report CSL-111, SRI International (1980) also in Formal Languages Theory: Perspectives and Open Problems, R. Book, Ed., Academic Press, 1980, pp. 349–405.
IRANI, K.B. and SHIN, D.G. A many-sorted resolution based on an extension of a first-order language. In Proceedings Ninth IJCAI (Los Angeles 1985), pp. 1175–1177.
KNUTH, D. and BENDIX, P. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra, J. Leech, Ed., 1970.
PLOTKIN, G. Building-in equational theories. Machine Intelligence 7 (1972), pp. 73–90.
ROBINSON, J.A. A machine-oriented logic based on the resolution principle, J.ACM 12, 1 (1965), pp. 23–41, also in [18].
SCHMIDT-SCHAUSS, M. A many-sorted calculus with polymorphic functions based on resolution and paramodulation. In Proceedings Ninth IJCAI (Los Angeles 1985), pp. 1162–1168.
SCHMIDT-SCHAUSS, M. Unification in Many-Sorted Equational Theories. In Proceedings Eight CADE (Oxford 1986), this volume.
SIEKMANN, J. Universal unification. In Proceedings Seventh CADE (Napa 1984), Lecture Notes in Computer Science 170, pp. 1–42.
SIEKMANN, J. and WRIGHTSON, G., Eds., Automation of Reasoning-Classical Papers on Computational Logic 1, Springer, 1983.
STICKEL, M. E. Automated deduction by theory resolution. In Proceedings Ninth IJCAI (Los Angeles 1985), pp. 1181–1186, revised version in J. Automated Reasoning 1, 4 (1985), pp. 333–355.
STICKEL, M. E. Schubert's Steamroller Problem: Formulations and Solutions. J. Automated Reasoning 2, 1 (1986), pp. 89–101.
WALTHER C. A many-sorted calculus based on resolution and paramodulation. In Proceedings Eight IJCAI (Karlsruhe 1983), pp. 882–891.
WALTHER, C. Unification in many-sorted theories. In Advances in Artificial Intelligence — Proceedings Sixth ECAI (Pisa 1984), T. O'Shea, Ed., North-Holland 1985, pp. 383–392.
WALTHER, C. A mechanical solution of Schubert's Steamroller by many-sorted resolution. In Proceedings Fourth AAAI (Austin 1984), pp. 330–334, revised version in Artificial Intelligence 26, 2 (1985), pp. 217–224.
WALTHER, C. A classification of unification problems in many-sorted theories. Interner Bericht 10/85, Universität Karlsruhe, Inst. f. Informatik I (1985), pp. 1–43.
WOS, L. and ROBINSON, G. Maximal models and refutation completeness: semidecision procedures in automatic theorem proving. In Wordproblems, Boone, W.W., Cannonito, F.B. Lyndon, R.C., Eds., North-Holland, 1973, also in [18].
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Walther, C. (1986). A classification of many-sorted unification problems. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_117
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_117
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive