Abstract
We introduce E-unification, weak E-unification, E-upper bound, E-lower bound, and E-generalization problems, and the corresponding notions of unification, weak unification, upper bound, lower bound, and generalization type of an equational theory. When defining instantiation preorders on solutions of these problems, one can compared substitutions w.r.t. their behaviour on all variables or on finite sets of variables. We shall study the effect which these different instantiation preorders have on the existence of most general or most specific solutions of E-unification, weak E-unification, and E-generalization problems. In addition, we shall elucidate the subtle difference between most general unifiers and coequalizers, and we shall consider generalization in the class of commutative theories.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
7 References
Baader, F. (1989). Unification in Commutative Theories. J. Symbolic Computation 8.
Baader, F. (1989a). Unification Properties of Commutative Theories: A Categorical Treatment. Proceedings of the Summer Conference on Category Theory and Computer Science, LNCS 389.
Baader, F. (1989b). Characterizations of Unification Type Zero. Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, RTA 89, LNCS 355.
Baader, F. (1990). Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems. SEKI Report SR-90-02, Universität Kaiserslautern.
Baader, F. (1990a). Unification in Commutative Theories, Hilbert's Basis Theorem and Gröbner Bases. SEKI Report SR-90-01, Universität Kaiserslautern.
Baader, F., Büttner, W. (1988). Unification in Commutative Idempotent Monoids. Theor. Comp. Sci. 56.
Eder, E. (1985). Properties of Substitutions and Unifications. J. Symbolic Computation 1.
Goguen, J.A. (1988). What is Unification? Technical Report, Computer Science Laboratory SRI International, SRI-CSL-88-2.
Huet, G. (1980). Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. J. ACM 27.
Mac Lane, S. (1971). Categories for the Working Mathematician. Heidelberg: Springer-Verlag.
Nutt, W. (1990). Unification in Monoidal Theories. Proceedings of the 10th International Conference on Automated Deduction, CADE 90, LNCS 449.
Oeljeklaus, E., Remmert, R. (1974). Lineare Algebra I. Berlin: Springer-Verlag.
Ohlbach, H.J. (1990). Abstraction Tree Indexing for Terms. Proceedings of the 9th European Conference on Artificial Intelligence, ECAI 90.
Plotkin, G. (1970). A Note on Inductive Generalization. Machine Intelligence 5.
Plotkin, G. (1972). Building in Equational Theories. Machine Intelligence 7.
Pottier, L. (1989). Algorithmes de completion et generalisation en logique du premier ordre. These de Doctorat Sciences, Universite de Nice-Sophia Antipolis LISAN-CNRS.
Robinson, J.A. (1965). A Machine-Oriented Logic Based on the Resolution Principle. J. ACM 12.
Rydeheard, D.E., Burstall, R.M. (1985). A Categorical Unification Algorithm. Proceedings of the Workshop on Category Theory and Computer Programming, LNCS 240.
Siekmann, J. (1989). Unification Theory. J. Symbolic Computation 7, Special Issue on Unification.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baader, F. (1991). Unification, weak unification, upper bound, lower bound, and generalization problems. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_88
Download citation
DOI: https://doi.org/10.1007/3-540-53904-2_88
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53904-9
Online ISBN: 978-3-540-46383-2
eBook Packages: Springer Book Archive