Abstract
In the literature several methods have hitherto been used to show that an equational theory has unification type zero. These methods depend on conditions which are candidates for alternative characterizations of unification type zero. In this paper we consider the logical connection between these conditions on the abstract level of partially ordered sets. Not all of them are really equivalent to type zero.
The conditions may be regarded as tools which can be used to determine the unification type of given theories. They are also helpful in understanding what makes a theory to be of type zero.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
6. References
Baader, F. (1986). The Theory of Idempotent Semigroups is of Unification Type Zero. J. Automated Reasoning 2.
Baader, F. (1987). Unification in Varieties of Idempotent Semigroups. Semigroup Forum 36.
Baader, F. (1988). A Note on Unification Type Zero. Information Processing Letters 27.
Bürckert, H.J. (1987). Matching — A Special Case of Unification? SEKI Technical Report, Universität Kaiserslautern.
Bürckert, H.J., Herold, A., Schmidt-Schauß, M. (1987). On Equational Theories, Unification and Decidability. Proceedings of the RTA '87 Bordeaux (France). Springer Lec. Notes Comp. Sci. 256.
Büttner, W. (1986). Unification in the Data Structure Multiset. J. Automated Reasoning 2.
Fages, F., Huet, G. (1983). Complete Sets of Unifiers and Matchers in Equational Theories. Proceedings of the CAAP '83 Pisa (Italy). Springer Lec. Notes Comp. Sci. 159.
Fages, F., Huet, G. (1986). Complete Sets of Unifiers and Matchers in Equational Theories. Theor. Comp. Sci. 43.
Plotkin, G. (1972). Building in Equational Theories. Machine Intelligence 7.
Schmidt-Schauß, M. (1986). Unification under Associativity and Idempotence is of Type Nullary. J. Automated Reasoning 2.
Schmidt-Schauß, M. (1986a). Unifikation Properties of Idempotent Semigroups. SEKI Technical Report, Universität Kaiserslautern.
Siekmann, J. (1988). Unification Theory. To appear in J. Symbolic Computation.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baader, F. (1989). Characterizations of unification type zero. In: Dershowitz, N. (eds) Rewriting Techniques and Applications. RTA 1989. Lecture Notes in Computer Science, vol 355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51081-8_96
Download citation
DOI: https://doi.org/10.1007/3-540-51081-8_96
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51081-9
Online ISBN: 978-3-540-46149-4
eBook Packages: Springer Book Archive