Abstract
Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of term rewriting systems. Reasoning by the rewriting induction is based on the noetherian induction on some reduction order. Thus, when the given conjecture is not orientable by the reduction order in use, any proof attempts for that conjecture fails; also conjectures such as a commutativity equation are out of the scope of the rewriting induction because they can not be oriented by any reduction order. In this paper, we give an enhanced rewriting induction which can deal with non-orientable conjectures. We also present an extension which intends an incremental use of our enhanced rewriting induction.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Resolution of Equations in Algebraic Structure, vol. 2, pp. 1–30. Academic Press, London (1989)
Bouhoula, A.: Automated theorem proving by test set induction. Journal of Symbolic Computation 23, 47–77 (1997)
Bouhoula, A., Kounalis, E., Rusinowitch, M.: Automated mathematical induction. Journal of Logic and Computation 5(5), 631–668 (1995)
Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1979)
Dershowitz, N., Reddy, U.S.: Deductive and inductive synthesis of equational programs. Journal of Symbolic Computation 15, 467–494 (1993)
Huet, G., Hullot, J.-M.: Proof by induction in equational theories with constructors. Journal of Computer and System Sciences 25(2), 239–266 (1982)
Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in theories without constructors. Information and Computation 82, 1–33 (1989)
Kapur, D., Narendran, P., Zhang, H.: Automating inductionless induction using test sets. Journal of Symbolic Computation 11(1–2), 81–111 (1991)
Koike, H., Toyama, Y.: Inductionless induction and rewriting induction. Computer Software 17(6), 1–12 (2000) (in Japanese)
Musser, D.R.: On proving inductive properties of abstract data types. In: Proc. of the 7th Annual ACM Symposium on Principles of Programming Languages, pp. 154–162. ACM Press, New York (1980)
Reddy, U.S.: Term rewriting induction. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol. 449, pp. 162–177. Springer, Heidelberg (1990)
Sakamoto, K., Aoto, T., Toyama, Y.: Fusion transformation based on rewriting induction. In: Proc. of the JSSST 21th Annual Conference, 2B-3 (2004) (in Japanese)
Terese.: Term Rewriting Systems. Cambridge University Press, Cambridge (2003)
Toyama, Y.: How to prove equivalence of term rewriting systems without induction. Theoretical Computer Science 90(2), 369–390 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aoto, T. (2006). Dealing with Non-orientable Equations in Rewriting Induction. In: Pfenning, F. (eds) Term Rewriting and Applications. RTA 2006. Lecture Notes in Computer Science, vol 4098. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11805618_18
Download citation
DOI: https://doi.org/10.1007/11805618_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-36834-2
Online ISBN: 978-3-540-36835-9
eBook Packages: Computer ScienceComputer Science (R0)