Abstract
A framework for rewriting with membership, equality, and inequality constraints is presented. A ground completion procedure is described which modifies the standard critical pair lemma. One consequence is the desire to rewrite terms in a set represented by a grammar, which leads to strong requirements on the conditional rules. Examples of the use of a completed constrained term rewriting system are presented, including an instance of an inductive theorem.
This research supported in part by the National Science Foundation under Grant CCR-90-24271.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
B. Bogaert and S. Tison. Automata with Equality Tests. Technical Report IT 207, Laboratoire d'Informatique Fondamental de Lille, USTL, Lille, France February 1991.
H. Comon. Rewriting with Membership Constraints. Draft, 1992.
H. Comon and C. Delor. Equational Formulas in Order-Sorted Algebras. Proc. ICALP, 1990.
H. Comon and P. Lescanne. Equational Problems and Disunification. J. Symbolic Computation 7, pages 371–425, 1989.
N. Dershowitz. Completion and Its Applications. In H. Aït-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures 2: Rewriting Techniques, chapter 2, pages 31–86. Academic Press, New York, 1989.
A. J. J. Dick and P. Watson. Order-sorted Term Rewriting. Computer Journal 34, pages 16–19, 1990.
J. Doner. Tree Acceptors and Some of Their Applications, Journal of Computer and System Sciences 4, pages 406–451, 1970.
A. M. Frisch. The Substitutional Framework for Sorted Deduction: Fundamental Results on Hybrid Reasoning. Artificial Intelligence 49, pages 161–198, 1991.
J. A. Goguen and J. Meseguer, Completeness of Many-sorted Equational Logic. SIGPLAN Notices 16, pages 24–32, 1981.
D. E. Knuth and P. B. Bendix, Simple Word Problems in Universal Algebras, In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, U. K. 1970.
C. Kirchner and P. Lescanne. Solving Disequations. Proc. 2nd IEEE Symp.on Logic in Computer Science, Ithaca, NY, pages 347–352, 1987.
A. Martelli, C. Moiso, and G. F. Rossi. An Algorithm for Unification in Equational Theories. Proc. IEEE Symp. on Logic in Computer Science, Salt Lake City, UT, September 1986.
G. Smolka, W. Nutt, J. A. Goguen and J. Meseguer. Order-Sorted Equational Computation. In H. Aït-Kaci and M Nivat, editors, Resolution of Equations in Algebraic Structures, Vol 2, Rewriting Techniques, pages 297–367, Academic Press, 1989.
Y. Toyama. Confluent Term Rewriting Systems with Membership Conditions. In S.Kaplan and J.P. Jouannaud, editors, Lecture Notes in Computer Science, 308, Conditional Term Rewriting Systems 1987 Proceedings pages 228–241, Springer Verlag 1987.
T. E. Uribe. Sorted Unification Using Set Constraints. In D. Kapur, editor, Lecture Notes in Computer Science, 11th International Conference on Automated Deduction, Springer-Verlag,1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hoot, C. (1993). Completion for constrained term rewriting systems. In: Rusinowitch, M., Rémy, JL. (eds) Conditional Term Rewriting Systems. CTRS 1992. Lecture Notes in Computer Science, vol 656. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56393-8_31
Download citation
DOI: https://doi.org/10.1007/3-540-56393-8_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56393-8
Online ISBN: 978-3-540-47549-1
eBook Packages: Springer Book Archive