Abstract
We present a completion procedure (called MKB) which works with multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard Kuuth-Bendix completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structure consisting of a pair s: t of terms associated with the information to show which processes contain the rule s → t (or t → s) and which processes contain the equation s ↔ t. The idea is based on the observation that some of the inferences made in the processes are closely related, so we can design inference rules that simulate multiple KB inferences in several processes all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Avenhaus J. and Madlener, K., Term rewriting and equational reasoning, Banerji, R.B. ed., Formal Techniques in Artificial Intelligence: A Sourcebook, North-Holland, 1–44, 1990.
Bachmair, L., Dershowitz, N., and Hsiang, J., Orderings for equational proofs, Proc. Symp. on Logic in Computer Science, 346 357, 1986.
Bachmair, L., Canonical Equational Proofs, Birkhäuser, 1991.
Dershowitz, N., Completion and its applications, Aït-Kaci, H. and Nivat, M. eds., Resolution of Equations in Algebraic Structures, Vol.2: Rewriting Techniques, Academic Press, 31 85, 1989.
Dershowitz, N. and Jouannaud, J.-P., Rewrite systems, van Leeuwen, J. ed., Handbook of Theoretical Computer Science, vol. B, North-Holland, 243 320, 1990.
Huet, G. and Oppen, D. C., Equations and rewrite rules: a survey, Book, R. ed., Formal Language Theory: Perspectives and Open Problems, Academic Press, 349 405, 1980.
Huet, G., A complete proof of correctness of the Knuth and Bendix completion algorithm, J. Comput. Syst. Sci. 23, 11 21, 1981.
Klop, J.W., Term rewriting systems, Abramsky, S., et al. eds., Handbook of Logic in Computer Science, vol. II, Oxford Univ. Press, 1 116, 1992.
Knuth, D.E. and Bendix, P.B., Simple word problems in universal algebras, Leech, J. ed., Computational Problems in Abstract Algebra, Pargamon Press, 263 297, 1970.
Lescanne, P., Completion procedures as transition rules + control, Proc. TAP-SOFT (vol. 1), Lect. Notes in Comput. Sci. 351, 28 41, 1989.
Plaisted, D. A., Equational reasoning and term rewriting systems, Gabbay, D. M. et al. eds., Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 1, Oxford Univ. Press, 274 367, 1993.
Steinbach, J. and Kühler, U., Check your ordering termination proofs and open problems, SEKI report, SR-90-25 (SFB), 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kurihara, M., Kondo, H., Ohuchi, A. (1995). Completion for multiple reduction orderings. In: Hsiang, J. (eds) Rewriting Techniques and Applications. RTA 1995. Lecture Notes in Computer Science, vol 914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59200-8_48
Download citation
DOI: https://doi.org/10.1007/3-540-59200-8_48
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59200-6
Online ISBN: 978-3-540-49223-8
eBook Packages: Springer Book Archive