Abstract
Contextual rewriting as a generalization of conditional rewriting has been studied in different forms. We show that contextual rewriting is a powerful simplification rule for the first-order theorem proving with equality and preserves the refutational completeness of many reasoning systems. After comparing definitions of contextual rewriting by Boyer-Moore, Remy, Ganzinger and Zhang-Kapur, we show that the definition of Zhang-Kapur is more suitable for implementation because it is natural to organize the context as a ground term rewriting system. We provide a detailed procedure for simplying clauses using contextual rewriting. We also provide a solution on how to handle variables which appear only in the condition of a conditional rewrite rule.
Partially supported by the National Science Foundation Grants no. CCR-9009414, INT-9016100 and CCR-9202838.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Boyer, R.S., Moore, J. S.: (1979) A Computational Logic. Academic Press, New York.
Bronsard, F., Reddy, U.S.: (1991) Conditional rewriting in Focus. In Kaplan, S., Okada, N. (eds): Procs. of Second International CTRS Workshop. pp. 2–13. Springer-Verlag, Berlin.
Bronsard, F., Reddy, U.S.: (1992) Reduction techniques for first-order reasoning. In Rusinowitch, M., Remy, J.L.: (eds): Procs. of Third International CTRS Workshop.
Dershowitz, N.: (1982) Ordering for term-rewriting systems. Theoretical Computer Science 17(3), 279–301.
Dershowitz, N., Jouannaud J.P.: (1990) Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pages 243–320, North-Holland, Amsterdam.
Ganzinger, H.: (1987) A completion procedure for conditional equations. In Kaplan, S., Jouannaud, J.-P. (eds) Proc. of Conditional Term Rewriting Systems. Lecture Notes in Computer Science, vol. 308. pp. 62–83.
Hsiang, J., Rusinowitch, M.: (1986) A new method for establishing refutational completeness in theorem proving. In: Siekmann, J.H. (ed.): Proc. of 8th conference on automated deduction, Lecture Notes in Computer Science 230, Springer, pp. 141–152
Kaplan S.: (1984) Fair conditional term rewriting systems: unification, termination and confluence. Technical Report, LRI, Orsay.
Kapur, D., Zhang, H.: (1989) An overview of RRL: Rewrite Rule Laboratory. In: Dershowitz, N. (ed.): Proc. of the third international conference on rewriting techniques and its applications. Lecture Notes in Computer Science 355, Springer. pp. 513–529.
Knuth, D., Bendix, P.: (1970) Simple word problems in universal algebras. In: Leech, (ed.) Computational problems in abstract algebra. New York: Pergamon Press. pp. 263–297.
Lankford, D.S.: (1979) Some new approaches to the theory and applications of conditional term rewriting systems. Report MTP-6, Dept. of Mathematics, Lousiana Tech University, Ruston, LA.
Remy, J.L.: (1982) Etudes des systemes reecriture conditionelles et applications aux types abstraits algebriques. These d'etat, Universite de Nancy I, Nancy, France.
Zhang, H.: (1988) Reduction, superposition and induction: automated reasoning in an equational logic. Ph.D. Thesis, Department of Computer Science, Rensselaer Polytechnic Institute, Troy, NY.
Zhang, H., Kapur, D.: (1988) First-order logic theorem proving using conditional rewrite rules. In: Lusk, E., Overbeek, lt., (eds.): Proc. of 9th international conference on automated deduction. Lecture Notes in Computer Science 310, Springer, pp. 1–20.
Zhang, H., Hua, X.: (1992) Proving Ramsey theorem by cover-set induction: a case and comparison study. Presented at Second International Symposium on Artificial Intelligence and Mathematics. Fort Lauderdale, Florida.
Zhang, H., Remy, J.L.: (1985) Contextual rewriting. In Jouannaud, J.P. (ed.): Proc. of 1st International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 202, Springer. pp. 1–20.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, H. (1993). Implementing contextual rewriting. 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_28
Download citation
DOI: https://doi.org/10.1007/3-540-56393-8_28
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