Abstract
We have described briefly a proof manager called FRI, which supports the cover set induction method of RRL. We believe that FRI makes the cover set method more powerful and applicable to a wider class of equational theories for automating inductive proofs. Without FRI, we could not obtain a proof of the Chinese Remainder theorem [9].
Any successful inductive prover must be based on heuristics, which involve at least the following operations: (a) choice of induction schemes, (b) use of induction hypotheses, (c) conjecturing lemmas, (d) generalization of induction formulas, (e) simplification strategies. In addition to the heuristics provided by RRL, FRI provides the facilities to perform any of the operations listed above.
FRI can also help us to develop new heuristics for further automating cover set induction. In fact, when we started to work on Ramsey's theorem [8], RRL could not prove each lemma of Ramsey's theorem automatically; they were proved semi-automatically with the assistance of FRI. The semi-automatically generated proof inspired us to add new techniques to increase the automatic power of RRL. Finally, we were able to obtain an automatic proof of Ramsey's theorem.
In the near future, we will further improve FRI and plan to integrate FRI with the TECTON system developed by Kapur et al. so that proof trees created by FRI can be displayed graphically in a hypertext environment.
Partially supported by the National Science Foundation Grants no. CCR-9009414 and INT-9016100.
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
Boyer, R.S., Moore, J.S.: (1979) A computational logic. New York: Academic Press.
Erickson, R.W., Musser, D.R.: (1980) The AFFIRM theorem prover: proof forests and management of large proofs. Proc. 7th Principles of Programming Languages.
Hua, X., Zhang, H.: (1991) Axiomatic semantics of a hardware specification language. Submitted to the Second IEEE Great Lakes Symposium on VLSI, Kalamazoo, MI, February 1992.
Kapur, D., Zhang, H.: (1989) An overview of RRL: Rewrite Rule Laboratory. Proc. of the third International Conference on Rewriting Techniques and its Applications (RTA-89), April 1989, Chapel Hill, NC, Springer Verlag LNCS 355, 513–529.
Kaufmann, M.: (1988) An interactive enhancement to the Boyer-Moore theorem prover. Proc. of Ninth International Conference on Automated Deduction (CADE-9), Argonne, IL, May 1988. Springer-Verlag LNCS 310, pp. 735–736.
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., Guha, A., Hua, X.: (1991) Using algebraic specifications in Floyd-Hoare assertions. In: Rus, T. (ed.): Proc. of Second International Conference on Algebraic Methodology and Software Technology, Iowa City, Iowa.
Zhang, H., Hua, X.: (1991) Proving Ramsey theorem by cover-set induction: a case and comparison study. Accepted for presentation at Second International Symposium on Artificial Intelligence and Mathematics. Fort Lauderdale, Florida.
Zhang, H., Hua, X.: (1991) A computer proof of the Chinese remainder theorem. Submitted to CADE-92.
Zhang, H., Kapur, D., Krishnamoorthy, M.S.: (1988) A mechanizable induction principle for equational specifications. Proc. of Ninth International Conference on Automated Deduction (CADE-9), Argonne, IL, May 1988. Springer-Verlag LNCS 310, pp. 250–265.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hua, X., Zhang, H. (1992). FRI: Failure-resistant induction in RRL. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_205
Download citation
DOI: https://doi.org/10.1007/3-540-55602-8_205
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55602-2
Online ISBN: 978-3-540-47252-0
eBook Packages: Springer Book Archive