×

Implicit induction in conditional theories. (English) Zbl 0819.68114

Summary: We propose a new procedure for proof by induction in conditional theories where case analysis is simulated by term rewriting. This technique reduces considerably the number of variables of a conjecture to be considered by applying induction schemes. Our procedure is presented as a set of inference rules whose correctness has been formally proved. Moreover, when the axioms are ground convergent and the functions are completely defined, it is possible to apply the system for refuting conjectures. The procedures is even refutationally complete for conditional equations with Boolean preconditions over free constructors. The method is entirely implemented in the power SPIKE. This system has solved interesting problems in a completely automatic way, that is, without interaction with the user and without ad hoc heuristics. It has also proved the challenging Gilbreath card trick, with only two easy lemmas.

MSC:

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

Software:

SPIKE; Coq
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bachmair, L.: Proof by consistency in equational theories, inProc. 3rd IEEE Sympos. Logic in Computer Science, Cambridge, Mass., USA, 1988, pp. 228-233.
[2] Basin, D. and Walsh, T.: Difference unification, inProc. 13th IJCAI, Morgan Kaufmann, Vol. 1, 1993, pp. 116-122.
[3] Bevers, E.: Automated reasoning in conditional algebric specifications: Termination and proof by consistency, PhD Thesis, Katholieke Universiteit Leuven, Belgium, 1993.
[4] Bouhoula, A.: Preuves automatiques par récurrence dans les théories conditionnelles, PhD Thesis, Université de Nancy I, 1994.
[5] Bouhoula, A. and Rusinowitch, M.: Automatic case analysis in proof by induction, in Ru?ena Bajcsy (ed.),Proc. 13th Internat. Joint, Conf. Artificial Intellignece, Chambéry (France), Volume 1, Morgan Kaufmann, 1993, pp. 88-94.
[6] Bouhoula, A., Kounalis, E., and Rusinowitch, M.: Automated mathematical induction, Technical Report 1636, INRIA, 1992. · Zbl 0832.68095
[7] Bouhoula, A., Kounalis, E. and Rusinowitch, M.: SPIKE: An automatic theorem prover, inProc. of LPAR’92, Vol. 624 of LNAI, Springer-Verlag, 1992.
[8] Boyer, R. S. and Moore, J. S.:A Computational Logic, Academic Press, New York, 1979. · Zbl 0448.68020
[9] Bronsard, F. and Reddy, S.: Conditional rewriting in focus, in S. Kaplan and M. Okada (eds),Proc. 2nd Workshop on Conditional and Typed Rewriting Systems, Vol. 516 of LNCS. Springer-Verlag, 1990.
[10] Bundy, A., Van Harmelen, F., Smaill, A., and Ireland, A.: Extensions to the rippling-out tactic for guiding inductive proofs, in M. E. Stickel (ed.),Proc. 10th Internat. Conf. on Automated Deduction, Vol. 449 of LNAI, Springer-Verlag, 1989, pp. 132-146.
[11] Chadha, R. and Plaisted, D. A.: Mechanizing mathematical induction,Presented at the Second International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, 1992.
[12] Dershowitz, N. and Jouannaud, J.-P.: Rewrite system, in J. van Leuven (ed.),Handbook of Theoretical Computer Science, Elsevier Science, 1990. · Zbl 0900.68283
[13] Dershowitz, N., Okada, M., and Sivakumar, G.: Canonical conditional rewrite systems, inProc. 9th Internat. Conf. on Automated Deduction, Argonne, Ill., USA, Vol. 310 of LNCS. Springer-Verlag, 1988. · Zbl 0667.68043
[14] Fribourg, L.: A strong restriction of the inductive completion procedure, inProc. 13th Internat. Colloquium on Automata, Languages and Programming, Vol. 226 of LNCS, Springer-Verlag, 1986, pp. 105-115.
[15] Guttag, J.: Abstract data types and software validation,Communications of the ACM,21 (1978), 1048-1064. · Zbl 0387.68012 · doi:10.1145/359657.359666
[16] Huber, M.: Testmengen für Grundreduzierbarkeit: Konstruktionen, Komplikationen, Korollare, Diplomarbeit, Technische Universität, Berlin, 1991.
[17] Huet, G. and Hullot, J.-M.: Proofs by induction in equational theories with constructors,J. Computer and System Sciences,25(2) (1982), 239-266. · Zbl 0532.68041 · doi:10.1016/0022-0000(82)90006-X
[18] Huet, G.: The Gilbreath trick: A case study in axiomatisation and proof development in the coq proof assistant, Technical Report 1511, INRIA, 1991.
[19] Jouannaud, J.-P. and Kounalis, E.: Proof by induction in equational theories without constructors, inProc. 1st IEEE Symp. on Logic in Computer Science, Cambridge, Mass., USA, 1986, pp. 358-366.
[20] Kapur, D. and Musser, D.: Proof by consistency,Artificial Intelligence 31(2) (1987), 125-157. · Zbl 0631.68073 · doi:10.1016/0004-3702(87)90017-8
[21] Kounalis, E. and Rusinowitch, H.: On word problems in Horn logic, in J.-P. Jouannaud and S. Kaplan (eds),Proc. 1st Internat. Workshop on Conditional Term Rewriting Systems, Orsay, France, Vol. 308, of LCNS, Springer-Verlag, 1987, pp. 144-160, See also the extended version published inJ. Symposium Computation 11 (1&2) (1991). · Zbl 0723.68100
[22] Kounalis, E. and Rusinowitch, M.: A mechanization of conditional reasoning, inFirst International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, 1990. · Zbl 0744.68114
[23] Kounalis, E. and Rusinowitch, M.: Mechanizing inductive reasoning, inProc. American Association for Artificial Intelligence Conference, Boston, AAAI Press and MIT Press, 1990, pp. 240-245.
[24] Kounalis, E.: Testing for inductive (co)-reducibility, in A. Arnold (ed.),Proc. 15th CAAP, Copenhagen, Denmark, Vol. 431 of LNCS, Springer-Verlag, 1990, pp. 221-238. · Zbl 0759.68048
[25] Musser, D. R.: On proving inductive properties of abstract data types, inProc. 7th ACM Symp. on Principles of Programming Languages, Association for Computing Machinery, 1980, pp. 154-162.
[26] Padawitz, P.:Computing in Horn Clause Theories, Springer-Verlag, 1988. · Zbl 0646.68004
[27] Reddy, U. S.: Term rewriting induction, in M. E. Stickel (ed.),Proc. 10th Internat. Conf. on Automated Deduction, Kaiserslautern, Germany, Vol. 449 of LNCS, Springer-Verlag, 1990, pp. 162-177.
[28] Wirth, C.-P. and Gramlich, B.: On notions of inductive validity for first-order equational clauses, in A. Bundy (ed.),12th Internat. Conf. on Automated Deduction, Vol. 814 of Lecture Notes in Artificial Intelligence, Springer-Verlag, 1994, pp. 162-176.
[29] Zhang, H., Kapur, D., and Krishnamoorthy, M. S.: A mechanizable induction principle for equational specifications, in E. Lusk and R. Overbeek (eds),Proc. 9th Internat. Conf. on Automated Deduction, Argonne, Ill., USA, Vol. 310 of LNCS, Springer-Verlag, 1988, pp. 162-181. · Zbl 0657.68103
[30] Zhang, H.: Implementing contextual rewriting, inProc. of the 3rd CTRS Workshop, Vol. 656 of LNCS, Springer-Verlag, 1993.
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.