Abstract
A unification algorithm for combinations of collapse-free equational theories with disjoint sets of function symbols is presented. The algorithm uses complete unification algorithms for the theories in the combination to compute complete sets of unifiers in the combined theory. It terminates if the algorithms for the theories in the combination terminate. The only restriction on the theories in the combination — apart from disjointness of function symbol sets — is that they must be collapse-free (i.e., they must not have axioms of the form t=x, where t is a non-variable term and x is a variable). This extends the class of equational theories for which the unification problem in combinations can be solved to collapse-free theories. The algorithm is based on a study of the properties of unifiers in combination of non-regular collapse-free theories.
Preview
Unable to display preview. Download preview PDF.
References
Birkhoff, G., ‘On the structure of abstract algebras', Proc. Cambridge Philos. Soc. 31, 433–454 (1935).
Eder, E., ‘Properties of Substitutions and Unifications', Journal of Symbolic Computation 1, (1985).
Fages, F., ‘Associative-Commutative Unification', in 7th Int. Conf. on Automated Deduction (ed. R. E. Shostak), Springer-Verlag, LNCS 170, 194–208 (1984).
Huet, G., ‘Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems', JACM 27, 1–12 (1980).
Huet, G. and Oppen, D.C., ‘Equations and Rewrite Rules: A Survey', in Formal Languages: Perspectives and Open Problems (ed. R. Book), Academic Press (1980).
Kirchner, C., ‘Méthodes et outils de conception systematique d'algorithmes d'unification dans les théories equationelles', Thèse de doctorat d'état, Université Nancy I (1985).
Lankford, D. and Brady, B., ‘On the Foundations of Applied Equational Logic', Department of Mathematics and Statistics, Louisiana Tech University (1984).
Lankford, D., Butler, G. and Brady, B., ‘Abelian Group Unification Algorithms for Elementary Terms', in Proc. of an NSF Workshop on the Rewrite Rule Laboratory (ed. J.V. Guttag, D. Kapur, and D.R. Musser), Report 84GEN008, General Electric Company, Schenectady, New-York, 101–108 (1984).
Livesey, M. and Siekmann, J., ‘Unification of A + C-terms (bags) and A + C + I − terms (sets)', Intern Bericht Nr. 5/76, Institut für Informatik I, Universität Karlsruhe (1976).
Nelson, G. and Oppen, D.C., ‘Simplification by cooperating decision procedures', ACM Trans. on Progr. Lang. and Syst. 1, 245–257 (1979).
Shostak, R.E., ‘Deciding Combinations of Theories', JACM 31, 1–12 (1984).
Siekmann, J., ‘Universal Unification', in 7th Int. Conf. on Automated Deduction (ed. R. E. Shostak), Springer-Verlag, LNCS 170, 1–42 (1984).
Stickel, M.E. A Unification Algorithm for Associative—Commutative Functions, JACM 28, 423–434 (1981).
Szabó, P., ‘Unifikationstheorie erster Ordnung', Thesis, Univ. Karlsruhe (1982).
Taylor, W., ‘Equational Logic', Houston Journal of Mathematics 5 (1979).
Vogel, E., ‘Morphismenunifikation', Diplomarbeit, Univ. Karlsruhe (1978).
Yelick, K., ‘Combining unification algorithms for confined equational theories', Proc. First Int. Conf. on Rewriting Techn. and Appl. (ed. J-P. Jouannaud), Springer-Verlag (1985).
Bürckert, H.-J., 'some Relationships between Unification, Restricted Unification, and Matching', SEKI-Report, Universität Kaiserslautern (1986).
Herold, A., ‘Combination of Unification Algorithms', MEMO SEKI-85-VIII-KL, Universität Kaiserslautern (1986).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tidén, E. (1986). Unification in combinations of collapse-free theories with disjoint sets of function symbols. 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_110
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_110
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