Abstract
The problem of combining matching algorithms for equational theories with disjoint signatures is studied. It is shown that the combined matching problem is in general undecidable but that it becomes decidable if all theories are regular. For the case of regular theories an efficient combination algorithm is developed. As part of that development we present a simple algorithm for solving the word problem in the combination of arbitrary equational theories with disjoint signatures.
This research was supported in part by NYNEX, NSF grant CCR-8706652, and by the Advanced Research Projects Agency of the DoD, monitored by the ONR under contract N00014-83-K-0125.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
H.-J. Bürckert: Some Relationships Between Unification, Restricted Unification and Matching, in: Proc. CADE-8, LNCS 230 (1986), 514–524.
H.-J. Bürckert: Matching — A Special Case of Unification?, Tech. Rep., Universität Kaiserslautern (1987).
N. Dershowitz, Z. Manna: Proving Termination with Multiset Orderings, CACM 22 (1979), 465–476.
K. Futatsugi, J.A. Goguen, J.-P. Jouannaud, J. Meseguer: Principles of OBJ2, in: Proc. 12th POPL (1985), 52–66.
S.J. Garland, J.V. Guttag: An Overview of LP, The Larch Prover, in: Proc. RTA-89, LNCS (1989).
A. Herold: Combination of Unification Algorithms, in: Proc. CADE-8, LNCS 230 (1986), 450–469.
A. Herold: Combination of Unification Algorithms in Equational Theories, Ph.D. Thesis, Fachbereich Informatik, Universität Kaiserslautern (1987).
G. Huet: Confluent Reductions: Abstract properties and Applications to Term Rewriting Systems, JACM 27, 4 (1980), 797–821.
G. Huet, D.C. Oppen: Equations and Rewrite Rules — A Survey, in: Formal Languages: Perspectives and Open Problems, R. Book (ed.), Academic Press (1982).
J.-P. Jouannaud, H. Kirchner: Completion of a Set of Rules Modulo a Set of Equations, SIAM Journal of Computing 15 (1986), 1155–1194.
C. Kirchner: Méthodes et outils de conception systématique d'algorithmes d'unification dans les théories équationnelles, Thèse d'état de l'Université de Nancy I (1985).
C. Kirchner, personal communication, June 1988.
P. Lescanne: REVE: A Rewrite Rule Laboratory, in: Proc. CADE-8, LNCS 230 (1986), 695–696.
G.E. Peterson, M.E. Stickel: Complete Sets of Reductions for Some Equational Theories, JACM, 28, 2 (1981), 233–264.
M. Schmidt-Schauß: Unification in a Combination of Arbitrary Disjoint Equational Theories, Tech. Rep., Universität Kaiserslautern (1987).
J.H. Siekmann: Universal Unification, in: Proc. CADE-7, LNCS 170 (1984).
E. Tidén: Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols, in: Proc. CADE-8, LNCS 230 (1986), 431–449.
E. Tidén: First-Order Unification in Combinations of Equational Theories, PhD Thesis, Department of Numerical Analysis and Computing Science, The Royal Institute of Technology, Stockholm (1986).
K. Yelick: Unification in Combinations of Collapse-Free Regular Theories, JSC 3 (1987), 153–181.
P. Szabó: Unifikationstheorie erster Ordnung, Ph.D. Thesis, Universität Karlsruhe (1982).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nipkow, T. (1989). Combining matching algorithms: The regular case. 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_118
Download citation
DOI: https://doi.org/10.1007/3-540-51081-8_118
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