Abstract
Kapur and Subramaniam [12] defined syntactical classes of equations where inductive validity can be decided automatically. However, these classes are quite restrictive, since defined function symbols with recursive definitions may only appear on one side of the equations. In this paper, we expand the decidable class of equations significantly by allowing both sides of equations to be expressed using defined function symbols. The definitions of these function symbols must satisfy certain restrictions which can be checked mechanically. These results are crucial to increase the applicability of decision procedures for induction.
This research was partially supported by an NSF ITR award CCR-0113611.
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
Autexier, S., Hutter, D., Mantel, H., Schairer, A.: Inka 5.0 – A Logical Voyager. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 207–211. Springer, Heidelberg (1999)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge Univ. Pr., Cambridge (1998)
Bouhoula, A., Rusinowitch, M.: Implicit Induction in Conditional Theories. Journal of Automated Reasoning 14, 189–235 (1995)
Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1979)
Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A Heuristic for Guiding Inductive Proofs. Artificial Intelligence 62, 185–253 (1993)
Bundy, A.: The Automation of Proof by Mathematical Induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 845–911 (2001)
Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Harcourt/ Academic Press, London (2001)
Giesl, J., Kapur, D.: Decidable Classes of Inductive Theorems. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 469–484. Springer, Heidelberg (2001)
Giesl, J., Kapur, D.: Deciding Inductive Validity of Equations. Technical Report AIB-2003-03 (2003), Available from http://aib.informatik.rwth-aachen.de
Kapur, D., Zhang, H.: An Overview of Rewrite Rule Laboratory (RRL). Journal of Computer and Mathematics with Applications 29, 91–114 (1995)
Kapur, D., Subramaniam, M.: New Uses of Linear Arithmetic in Automated Theorem Proving by Induction. Journal of Automated Reasoning 16, 39–78 (1996)
Kapur, D., Subramaniam, M.: Extending Decision Procedures with Induction Schemes. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 324–345. Springer, Heidelberg (2000)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)
Walther, C.: Mathematical Induction. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2. Oxford University Press, Oxford (1994)
Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A Mechanizable Induction Principle for Equational Specifications. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, Springer, Heidelberg (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giesl, J., Kapur, D. (2003). Deciding Inductive Validity of Equations. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-45085-6_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40559-7
Online ISBN: 978-3-540-45085-6
eBook Packages: Springer Book Archive