Abstract
Most of the work on the combination of unification algorithms for the union of disjoint equational theories has been restricted to algorithms which compute finite complete sets of unifiers. Thus the developed combination methods usually cannot be used to combine decision procedures, i.e., algorithms which just decide solvability of unification problems without computing unifiers. In this paper we describe a combination algorithm for decision procedures which works for arbitrary equational theories, provided that solvability of so-called unification problems with constant restrictions—a slight generalization of unification problems with constants—is decidable for these theories. As a consequence of this new method, we can for example show that general A-unifiability, i.e., solvability of A-unification problems with free function symbols, is decidable. Here A stands for the equational theory of one associative function symbol.
Our method can also be used to combine algorithms which compute finite complete sets of unifiers. Manfred Schmidt-Schauß' combination result, the until now most general result in this direction, can be obtained as a consequence of this fact. We also get the new result that unification in the union of disjoint equational theories is finitary, if general unification—i.e., unification of terms with additional free function symbols—is finitary in the single theories.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
F. Baader, K.U. Schulz, “Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures,” DFKI Research Report RR-91–33.
L. Bachmair, Proof Methods for Equational Theories, Ph.D. Thesis, Dept. of Comp. Sci., University of Illinois at Urbana-Champaign, 1987.
A. Boudet, “Unification in a Combination of Equational Theories: An Efficient Algorithm,” Proceedings of the 10th International Conference on Automated Deduction, LNCS 449, 1990.
A. Boudet, J.P. Jouannaud, M. Schmidt-Schauß, “Unification in Boolean Rings and Abelian Groups,” J. Symbolic Computation 8, 1989.
H.-J. Bürckert, “Some Relationships Between Unification, Restricted Unification, and Matching,” Proceedings of the 8th International Conference on Automated Deduction, LNCS 230, 1986.
H.-J. Bürckert, “A Resolution Principle for Clauses with Constraints,” Proceedings of the 10th International Conference on Automated Deduction, LNCS 449, 1990.
N. Dershowitz, J.P. Jouannaud, “Rewrite Systems,” In J. van Leeuwen (editor), Volume B of Handbook of Theoretical Computer Science, NorthHolland, 1990.
F. Fages, “Associative-Commutative Unification,” Proceedings of the 7th International Conference on Automated Deduction, LNCS 170, 1984.
A. Herold, “Combination of Unification Algorithms,” Proceedings of the 8th International Conference on Automated Deduction, LNCS 230, 1986.
A. Herold, J.H. Siekmann, “Unification in Abelian Semigroups,” J. Automated Reasoning 3, 1987.
J.M. Howie, An Introduction to Semigroup Theory, London: Academic Press, 1976.
J. Jaffar, J.L. Lassez, M. Maher, “A Theory of Complete Logic Programs with Equality,” J. Logic Programming 1, 1984.
J. Jaffar, J.L. Lassez, “Constraint Logic Programming,” Proceedings of 14th POPL Conference, Munich, 1987
J.P. Jouannaud, H. Kirchner, “Completion of a Set of Rules Modulo a Set of Equations,” SIAM J. Computing 15, 1986.
J.P. Jouannaud, C. Kirchner, “Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification,” In J.-L. Lassez, G. Plotkin (editors), Alan Robinson's Anniversary Book, 1991.
D. Kapur, P. Narendran, “Complexity of Unification Problems with Associative-Commutative Operators,” Preprint, 1991. To appear in J. Automated Reasoning.
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, France, 1985.
C. Kirchner, H. Kirchner, “Constrained Equational Reasoning,” Proceedings of SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ACM Press, 1989.
M. Livesey, J.H. Siekmann, “Unification of AC-Terms (bags) and ACITerms (sets),” Internal Report, University of Essex, 1975, and Technical Report 3-76, Universität Karlsruhe, 1976.
G.S. Makanin, “The Problem of Solvability of Equations in a Free Semigroup,” Mat. USSR Sbornik 32, 1977.
G. Plotkin, “Building in Equational Theories,” Machine Intelligence 7, 1972.
M. Schmidt-Schauß, “Combination of Unification Algorithms,” J. Symbolic Computation 8, 1989.
K.U. Schulz, “Makanin's Algorithm — Two Improvements and a Generalization,” CIS-Report 91-39, CIS, University of Munich, 1991.
J.H. Siekmann, “Unification Theory: A Survey,” in C. Kirchner (ed.), Special Issue on Unification, Journal of Symbolic Computation 7, 1989.
M. Stickel, “A Complete Unification Algorithm for Associative-Commutative Functions,” Proceedings of the International Joint Conference on Artificial Intelligence, 1975.
M.E. Stickel, “A Unification Algorithm for Associative-Commutative Functions,” J. ACM 28, 1981.
M.E. Stickel, “Automated Deduction by Theory Resolution,” J. Automated Reasoning 1, 1985.
E. Tiden, “Unification in Combinations of Collapse Free Theories with Disjoint Sets of Function Symbols,” Proceedings of the 8th International Conference on Automated Deduction, LNCS 230, 1986.
K. Yelick, “Unification in Combinations of Collapse Free Regular Theories,” J. Symbolic Computation 3, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baader, F., Schulz, K.U. (1992). Unification in the union of disjoint equational theories: Combining decision procedures. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_155
Download citation
DOI: https://doi.org/10.1007/3-540-55602-8_155
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55602-2
Online ISBN: 978-3-540-47252-0
eBook Packages: Springer Book Archive