Abstract
An algorithm is presented for solving equations in a combination of arbitrary theories with disjoint sets of function symbols. It is an extension of [3] in which the problem was treated for the combination of an arbitrary and a simple theory. The algorithm consists in a set of transformation rules that simplify a unification problem until a solved form is obtained. Each rule is shown to preserve solutions, and solved problems are unification problems in normal form. The rules terminate for any control that delays replacement until the end. The algorithm is more efficient than [13] because nondeterministic branching is performed only when necessary, that is when theory clashes or compound cycles are encountered.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A. Boudet. Unification dans les Mélanges de Théories Equationnelles. Ph. D. Thesis, Univ. Paris XI, Orsay, 1990.
L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., pages 346–357, June 1986.
A. Boudet, J.-P. Jouannaud, and M. Schmidt-Schauß. Unification in boolean rings and abelian groups. J. Symbolic Computation, 8:449–477, 1989.
H.-J. Bürckert. Matching, a special case of unification? J. Symbolic Computation, 8:523–536, 1989.
W. Büttner and H. Simonis. Preprint, Siemens AG, München, 1986. Embedding Boolean Expressions into Logic programming.
B. Brady D. S. Lankford, G. Butler. Abelian groups unification algorithms for elementary terms. In General Electric Workshop on the Rewrite Rule Laboratory, may 1984.
Nachum Dershowitz and Jean-Pierre Jouannaud. Handbook of Theoretical Computer Science, chapter Rewrite Systems. Volume B, North-Holland, 1990.
J. Hsiang and M. Rusinowitch. On word problems in equational theories. In Proc. 14th ICALP, Karlsruhe, LNCS 267, Springer-Verlag, July 1987.
C. Kirchner. Méthodes et Outils de Conception Systématique d'Algorithmes d'Unification dans les Théories equationnelles. Thèse d'Etat, Univ. Nancy, 1985.
A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982.
U. Martin and T. Nipkow. Unification in boolean rings. In Proc. 8th Conf. on Automated Deduction, Oxford, LNCS 230, Springer-Verlag, July 1986.
J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.
M. Schmidt-Schauß. Unification in a combination of arbitrary disjoint equational theories. In Proc. 9th Conf. on Automated Deduction, Argonne, LNCS 310, Springer-Verlag, May 1988.
R. E. Shostack. Deciding combinations of theories. Journal of the ACM, 31, 1984.
M. Stickel. A unification algorithm for associative-commutative functions. Journal of the ACM, 28(3):423–434, 1981.
E. Tidén. Unification in combinations of collapse-free theories with disjoint sets of function symbols. In Proc. 8th Conf. on Automated Deduction, Oxford, LNCS 230, Springer-Verlag, July 1986.
C. Yelick. Combining unification algorithms for confined equational theories. J. Symbolic Computation, 3(1), February 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boudet, A. (1990). Unification in a combination of equational theories: an efficient algorithm. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_95
Download citation
DOI: https://doi.org/10.1007/3-540-52885-7_95
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52885-2
Online ISBN: 978-3-540-47171-4
eBook Packages: Springer Book Archive