×

New uses of linear arithmetic in automated theorem proving by induction. (English) Zbl 0851.03002

The ‘cover set method’ is an algorithm for generating induction schemes for proof by explicit induction. It uses syntactic unification to generate schemes in a setting where functions are defined by finite sets of terminating rewrite rules. The authors provide a generalization based on semantic unification where a decision procedure for Presburger arithmetic is used to provide the semantic analysis. The unique prime factorization theorem of number theory is used as a nontrivial example to demonstrate how this generalization helps automate inductive theorem proving in the context of the theorem prover RRL.

MSC:

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

NQTHM; RRL; Tecton
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Boyer, R. S. and Moore, J S.: A Computational Logic, ACM Monographs in Computer Science, 1979. · Zbl 0448.68020
[2] Boyer, R. S.; Moore, J. S., A Computational Logic Handbook (1988), New York: Academic Press, New York · Zbl 0655.68117
[3] Boyer, R. S.; Moore, J. S., Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic, Machine Intelligence, 11, 83-157 (1988) · Zbl 0678.68091
[4] Dershowitz, N., Termination of rewriting, J. Symbolic Computation, 3, 69-116 (1987) · Zbl 0637.68035 · doi:10.1016/S0747-7171(87)80022-6
[5] Jouannaud, J.-P.; Kounalis, E., Automatic proofs by induction in theories without constructors, Information and Computation, 82, 1-33 (1989) · Zbl 0682.68032 · doi:10.1016/0890-5401(89)90062-X
[6] Kapur, D.: An automated tool for analyzing completeness of equational specifications, in Proc. Int. Symp. Software Testing and Analysis (ISSTA), Seattle, August 1994, pp. 28-43.
[7] Kapur, D., Musser, D. R., and Nie, X.: An overview of the Tecton proof system, in Theoret. Computer Science Journal, special issue on Formal Methods in Databases and Software Engineering (ed. V. Alagar), Vol. 133, October 1994, pp. 307-339. · Zbl 0938.68823
[8] Kapur, D.; Narendran, P.; Rosenkrantz, D.; Zhang, H., Sufficient-completeness, quasi-reducibility and their complexity, Acta Informatica, 28, 311-350 (1991) · Zbl 0721.68032 · doi:10.1007/BF01893885
[9] Kapur, D. and Nie, X.: Reasoning about numbers in Tecton, in Proc. 8th Int. Symp. Methodologies for Intelligent Systems (ISMIS’94), Charlotte, NC, October 1994, pp. 57-70.
[10] Kapur, D.; Zhang, H., An overview of Rewrite Rule Laboratory (RRL), J. Computer Math. Appl., 29, 2, 91-114 (1995) · doi:10.1016/0898-1221(94)00218-A
[11] Walther, C.: Combining induction axioms by machine, Proc. 12th Int. Joint Conf. Artificial Intelligence, Chambery, France, 1993.
[12] Zhang, H.: Reduction, superposition and induction: Automated reasoning in an equational logic, Ph.D. Thesis, Department of Computer Science, Rensselaer Polytechnic Institute, Troy, NY, 1988.
[13] Zhang, H., Kapur, D., and Krishnamoorthy, M. S.: A mechanizable induction principle for equational specifications, in Proc. 9th Int. Conf. Automated Deduction (CADE-9), Argonne, IL, LNCS 310, Springer-Verlag, 1988, pp. 250-265. · Zbl 0657.68103
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.