Abstract
Families of function definitions and conjectures based in quantifier-free decidable theories are identified for which inductive validity of conjectures can be decided by the cover set method, a heuristic implemented in a rewrite-based induction theorem prover Rewrite Rule Laboratory (RRL) for mechanizing induction. Conditions characterizing definitions and conjectures are syntactic, and can be easily checked, thus making it possible to determine a priori whether a given conjecture can be decided. The concept of a \(\mathcal{T}\)-based function definition is introduced that consists of a finite set of terminating complete rewrite rules of the form f(s 1,⋯,s m ) → r, where s 1,⋯,s m are interpreted terms from a decidable theory \(\mathcal{T}\), and r is either an interpreted term or has non-nested recursive calls to f with all other function symbols from \(\mathcal{T}\). Two kinds of conjectures are considered. Simple conjectures are of the form f(x 1,⋯,x m ) = t, where f is \(\mathcal{T}\)-based, x i ’s are distinct variables, and t is interpreted in \(\mathcal{T}\). Complex conjectures differ from simple conjectures in their left sides which may contain many function symbols whose definitions are \(\mathcal{T}\)-based and the nested order in which these function symbols appear in the left sides have the compatibility property with their definitions.
The main objective is to ensure that for each induction subgoal generated from a conjecture after selecting an induction scheme, the resulting formula can be simplified so that induction hypothesis(es), whenever needed, is applicable, and the result of this application is a formula in \(\mathcal{T}\). Decidable theories considered are the quantifier-free theory of Presburger arithmetic, congruence closure on ground terms (with or without associative-commutative operators), propositional calculus, and the quantifier-free theory of constructors (mostly, free constructors as in the case of finite lists and finite sequences). A byproduct of the approach is that it can predict the structure of intermediate lemmas needed for automatically deciding this subclass of conjectures. Several examples over lists, numbers and of properties involved in establishing the number-theoretic correctness of arithmetic circuits are given.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Gupta, A.: Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction. Ph.D. Thesis, Department of Computer Sci- ence, Carnegie Mellon University, Pittsburgh (1994)
Boyer, R.S., Moore, J S.: A Computational Logic. ACM Monographs in Computer Science (1979)
Boyer, R.S., Moore, J.S.: Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In: Hayes, J.E., Mitchie, D., Richards, J. (eds.) Machine Intelligence, vol. 11 (1988)
Fribourg, L.: Mixing list recursion and arithmetic. In: Proc. Seventh Symp. on Logic in Computer Science (1992)
Giesl, J., Kapur, D.: Decidable Classes of Inductive Theorems. Technical Report, Department of Computer Science, University of New Mexico (February 2000)
Kapur, D.: Automated tools for analyzing completeness of specifications. In: Proc. 1994 Intl. Symp. on Software Testing and Analysis (ISSTA), Seattle, WA, August 1994, pp. 28–43 (1994)
Kapur, D.: Rewriting, decision procedures and lemma speculation for automated hardware verification. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275. Springer, Heidelberg (1997)
Kapur, D., Nie, X.: Reasoning about numbers in Tecton. In: Raś, Z.W., Zemankova, M. (eds.) ISMIS 1994. LNCS, vol. 869. Springer, Heidelberg (1994)
Kapur, D., Subramaniam, M.: New uses of linear arithmetic in inductive theorem proving. J. Automated Reasoning 16(1-2), 39–78 (1996)
Kapur, D., Subramaniam, M.: Mechanically verifying a family of multiplier circuits. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 135–146. Springer, Heidelberg (1996)
Kapur, D., Subramaniam, M.: Mechanizing reasoning about arithmetic circuits: SRT division. In: Ramesh, S., Sivakumar, G. (eds.) FST TCS 1997. LNCS, vol. 1346, p. 103. Springer, Heidelberg (1997)
Kapur, D., Subramaniam, M.: Mechanical verification of adder circuits using powerlists. J. of Formal Methods in System Design (November 1998)
Kapur, D., Subramaniam, M.: Using an induction prover for verifying arithmetic circuits. J. of Software Tools for Technology Transfer. Springer (1999) (to appear)
Kapur, D., Zhang, H.: An overview of Rewrite Rule Laboratory (RRL). J. of Computer and Mathematics with Applications 29(2), 91–114 (1995)
Subramaniam, M.: Failure Analyses in Inductive Theorem Provers. Ph.D. Thesis, Department of Computer Science, University at Albany, State University of New York (1997)
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, pp. 250–265. Springer, Heidelberg (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapur, D., Subramaniam, M. (2000). Extending Decision Procedures with Induction Schemes. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_26
Download citation
DOI: https://doi.org/10.1007/10721959_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive