Abstract
In this paper we consider the class of theories for which solving unification problems is equivalent to solving systems of linear equations over a semiring. This class has been introduced by the authors independently of each other as commutative theories (Baader) and monoidal theories (Nutt). The class encompasses important examples like the theories of abelian monoids, idempotent abelian monoids, and abelian groups.
We identify a large subclass of commutative/monoidal theories that are of unification type zero by studying equations over the corresponding semiring. As a second result, we show with methods from linear algebra that unitary and finitary commutative/monoidal theories do not change their unification type when they are augmented by a finite monoid of homomorphisms, and how algorithms for the extended theory can be obtained from algorithms for the basic theory. The two results illustrate how using algebraic machinery can lead to general results and elegant proofs in unification theory.
Preview
Unable to display preview. Download preview PDF.
References
F. Baader, “Unification in Commutative Theories,” JSC 8, 1989.
F. Baader, “Unification Properties of Commutative Theories: A Categorical Treatment,” Proc. CTCS, LNCS 389, 1989.
F. Baader, Unification in Commutative Theories, Hilbert's Basis Theorem, and Gröbner Bases, SEKI-Report SR-90-01, Universität Kaiserslautern, Germany, 1990.
F. Baader, W. Nutt, Adding Homomorphisms to Commutative/Monoidal Theories or How Algebra Can Help in Equational Unification, Research Report RR-16-90, German Research Center for Artificial Intelligence (DFKI), Kaiserslautern, Germany, 1990.
C. Kirchner, F. Klay, “Syntactic Theories and Unification,” Proc. LICS 90, 1990.
M. Livesey, J. Siekmann, Unification of Bags and Sets, Report MEMO SEKI-76-II, Institut für Informatik I, Universität Karlsruhe, Germany, 1976.
W. Nutt, “Unification in Monoidal Theories,” presented at UNIF'88, Val d'Ajol, France, 1988.
W. Nutt, “Unification in Monoidal Theories,” Proc. 10th CADE, LNCS 449, 1990.
M. Schmidt-Schauß, “Combination of Unification Algorithms,” JSC 8, 1989.
J. H. Siekmann, “Unification Theory: A Survey,” JSC 7, 1989.
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., Nutt, W. (1991). Adding homomorphisms to commutative/monoidal theories or how algebra can help in equational unification. 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_91
Download citation
DOI: https://doi.org/10.1007/3-540-53904-2_91
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