×

Mechanically certifying formula-based Noetherian induction reasoning. (English) Zbl 1356.68202

Summary: In first-order logic, the formula-based instances of the Noetherian induction principle allow to perform effectively simultaneous, mutual and lazy induction reasoning. Compared to the term-based Noetherian induction instances, they are not directly supported by the current proof assistants.
We provide general formal tools for certifying formula-based Noetherian induction proofs by the Coq proof assistant, then show how to apply them to certify proofs of conjectures about conditional specifications, built with: i) a reductive rewrite-based induction system, and ii) a reductive-free cyclic induction system. The generation of reductive proofs and their certification process can be easily automatised, without requiring additional definitions or proof transformations, but may involve many ordering constraints to be checked during the certification process. On the other hand, the reductive-free proofs generate fewer ordering constraints, may involve more general specifications and the certification process is more effective. However, their proof generation is less automatic and the generated proofs need to be normalised before being certified. The methodology for certifying reductive-free cyclic induction proofs related to conditional specifications extends a previous approach used for implicit induction proofs and it can be easily adapted to certify any formula-based Noetherian induction reasoning.
In practice, the methodology has been implemented to automatically certify implicit induction proofs generated by the SPIKE theorem prover as well as reductive-free cyclic proofs built by the same system but in a less automatic way.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[2] Aoto, T., Dealing with non-orientable equations in rewriting induction, (Pfenning, F., RTA. RTA, Lect. Notes Comput. Sci., vol. 4098 (2006), Springer), 242-256 · Zbl 1151.68627
[3] Armando, A.; Rusinowitch, M.; Stratulat, S., Incorporating decision procedures in implicit induction, J. Symb. Comput., 34, 4, 241-258 (2002), A previous version appeared in: Calculemus 2001 (9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning), pp. 65-75 · Zbl 1037.68129
[4] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press
[5] Bachmair, L.; Ganzinger, H., Resolution theorem proving, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning (2001), Elsevier and MIT Press), 19-99 · Zbl 0993.03008
[6] Balaa, A.; Bertot, Y., Fix-point equations for well-founded recursion in type theory, (Aagaard, M.; Harrison, J., Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, Lect. Notes Comput. Sci., vol. 1869 (2000), Springer: Springer Berlin/Heidelberg), 1-16 · Zbl 0974.68183
[7] Barthe, G.; Courtieu, P., Efficient reasoning about executable specifications in Coq, (Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, Lect. Notes Comput. Sci., vol. 2410 (2002), Springer: Springer Berlin), 31-46 · Zbl 1013.68539
[8] Barthe, G.; Forest, J.; Pichardie, D.; Rusu, V., Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant, (Hagiya, M.; Wadler, P., Functional and Logic Programming. Functional and Logic Programming, Lect. Notes Comput. Sci., vol. 3945 (2006), Springer: Springer Berlin/Heidelberg), 114-129 · Zbl 1185.68616
[9] Barthe, G.; Stratulat, S., Validation of the JavaCard platform with implicit induction techniques, (Nieuwenhuis, R., RTA (Rewriting Techniques and Applications). RTA (Rewriting Techniques and Applications), Lect. Notes Comput. Sci., vol. 2706 (2003), Springer), 337-351 · Zbl 1038.68557
[10] Berregeb, N.; Bouhoula, A.; Rusinowitch, M., SPIKE-AC: a system for proofs by induction in associative-commutative theories, (Ganzinger, H., Rewriting Techniques and Applications. Rewriting Techniques and Applications, Lect. Notes Comput. Sci., vol. 1103 (1996), Springer: Springer Berlin/Heidelberg), 428-431
[11] Berregeb, N.; Bouhoula, A.; Rusinowitch, M., Observational proofs with critical contexts, (Fundamental Approaches to Software Engineering (1998)), 38-53
[12] Blanqui, F.; Koprowski, A., CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Math. Struct. Comput. Sci., 21, 4, 827-859 (2011) · Zbl 1223.68101
[13] Bouhoula, A., SPIKE: a system for sufficient completeness and parameterized inductive proofs, (Bundy, A., Automated Deduction — CADE-12. Automated Deduction — CADE-12, Lect. Notes Comput. Sci., vol. 814 (1994), Springer: Springer Berlin Heidelberg), 836-840
[14] Bouhoula, A., Using induction and rewriting to verify and complete parameterized specifications, Theor. Comput. Sci., 170, 170-171 (1996) · Zbl 0874.68198
[15] Bouhoula, A., Simultaneous checking of completeness and ground confluence for algebraic specifications, ACM Trans. Comput. Log., 10, 3, 1-33 (2009) · Zbl 1351.68171
[16] Bouhoula, A.; Jouannaud, J., Automata-driven automated induction, Inf. Comput., 169, 1, 1-22 (2001) · Zbl 1008.03009
[17] Bouhoula, A.; Kounalis, E.; Rusinowitch, M., SPIKE, an automatic theorem prover, (Logic Programming and Automated Reasoning (LPAR) (1992)), 460-462
[18] Bouhoula, A.; Kounalis, E.; Rusinowitch, M., Automated mathematical induction, J. Log. Comput., 5, 5, 631-668 (1995) · Zbl 0832.68095
[19] Bouhoula, A.; Rusinowitch, M., Observational proofs by rewriting, Theor. Comput. Sci., 275, 1-2, 675-698 (2002) · Zbl 1051.68085
[20] Boulton, R.; Slind, K., Automatic derivation and application of induction schemes for mutually recursive functions, (Lloyd, J.; Dahl, V.; Furbach, U.; Kerber, M.; Lau, K.-K.; Palamidessi, C.; Pereira, L.; Sagiv, Y.; Stuckey, P., Computational Logic — CL 2000. Computational Logic — CL 2000, Lect. Notes Comput. Sci., vol. 1861 (2000), Springer: Springer Berlin/Heidelberg), 629-643 · Zbl 0983.68533
[21] Boyer, R. S.; Moore, J. S., A Computational Logic Handbook (1988), Academic Press Professional · Zbl 0678.68091
[22] Boyer, R.; Moore, J. S., MJRTY—a fast majority vote algorithm, (Automated Reasoning: Essays in Honor of Woody Bledsoe (1991))
[23] Bronsard, F.; Reddy, U. S., Conditional rewriting in Focus, (Conditional and Typed Rewriting Systems (1991)), 1-13 · Zbl 1507.68144
[24] Bronsard, F.; Reddy, U.; Hasker, R., Induction using term orderings, (CADE (Conf. on Automated Deduction). CADE (Conf. on Automated Deduction), Lect. Notes Comput. Sci., vol. 814 (1994), Springer), 102-117 · Zbl 1433.68537
[25] Brotherston, J.; Simpson, A., Sequent calculi for induction and infinite descent, J. Log. Comput., 21, 6, 1177-1216 (2011) · Zbl 1242.03084
[26] Comon, H., Inductionless induction, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning (2001), Elsevier and MIT Press), 913-962 · Zbl 0994.03006
[27] Contejean, E.; Courtieu, P.; Forest, J.; Pons, O.; Urbain, X., Certification of automated termination proofs, (Frontiers of Combining Systems (2007)), 148-162 · Zbl 1148.68465
[28] Contejean, E.; Paskevich, A.; Urbain, X.; Courtieu, P.; Pons, O.; Forest, J., A3PAT, an approach for certified automated termination proofs, (Gallagher, J. P.; Voigtländer, J., PEPM - Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. PEPM - Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2010, Madrid, Spain, January 18-19, 2010 (2010), ACM), 63-72
[29] Courant, J., Proof reconstruction (1996), Research report RR96-26, LIP, preliminary version
[30] Deplagne, E.; Kirchner, C.; Kirchner, H.; Nguyen, Q. H., Proof search and proof check for equational and inductive theorems, (Automated Deduction - CADE-19. Automated Deduction - CADE-19, Lect. Notes Comput. Sci., vol. 2741 (2003)), 297-316 · Zbl 1278.68257
[31] Dershowitz, N., Orderings for term-rewriting systems, Theor. Comput. Sci., 17, 3, 279-301 (1982) · Zbl 0525.68054
[32] Dershowitz, N.; Reddy, U. S., Deductive and inductive synthesis of equational programs, J. Symb. Comput., 15, 5/6, 467-494 (1993) · Zbl 0791.68106
[33] Gonthier, G.; Asperti, A.; Avigad, J.; Bertot, Y.; Cohen, C.; Garillot, F.; Roux, S. L.; Mahboubi, A.; O’Connor, R.; Biha, S. O.; Pasca, I.; Rideau, L.; Solovyev, A.; Tassi, E.; Théry, L., A machine-checked proof of the Odd Order Theorem, (Blazy, S.; Paulin-Mohring, C.; Pichardie, D., Interactive Theorem Proving - 4th International Conference, Proceedings. Interactive Theorem Proving - 4th International Conference, Proceedings, ITP 2013, Rennes, France, July 22-26, 2013. Interactive Theorem Proving - 4th International Conference, Proceedings. Interactive Theorem Proving - 4th International Conference, Proceedings, ITP 2013, Rennes, France, July 22-26, 2013, Lect. Notes Comput. Sci., vol. 7998 (July 2013), Springer), 163-179 · Zbl 1317.68211
[34] Henaien, A.; Stratulat, S., Performing implicit induction reasoning with certifying proof environments, (Bouhoula, A.; Ida, T.; Kamareddine, F., Proceedings Fourth International Symposium on Symbolic Computation in Software Science. Proceedings Fourth International Symposium on Symbolic Computation in Software Science, Gammarth, Tunisia, 15-17 December 2012. Proceedings Fourth International Symposium on Symbolic Computation in Software Science. Proceedings Fourth International Symposium on Symbolic Computation in Software Science, Gammarth, Tunisia, 15-17 December 2012, Electronic Proceedings in Theoretical Computer Science, vol. 122 (2013), Open Publishing Association), 97-108
[35] Howe, D. J., Reasoning about functional programs in Nuprl, (Functional Programming, Concurrency, Simulation and Automated Reasoning. Functional Programming, Concurrency, Simulation and Automated Reasoning, Lect. Notes Comput. Sci., vol. 693 (1993), Springer Verlag), 145-164
[36] Kaliszyk, C., Validation des preuves par récurrence implicite avec des outils basés sur le calcul des constructions inductives (2005), Université Paul Verlaine: Université Paul Verlaine Metz, Master’s thesis
[38] Kapur, D.; Musser, D. R., Proof by consistency, Artif. Intell., 31, 2, 125-157 (1987) · Zbl 0631.68073
[39] Kapur, D.; Narendran, P.; Zhang, H., Proof by induction using test sets, (8th International Conference on Automated Deduction. 8th International Conference on Automated Deduction, Lect. Notes Comput. Sci., vol. 230 (1986), Springer), 99-117
[40] Kapur, D.; Subramaniam, M., Automating induction over mutually recursive functions, (Algebraic Methodology and Software Technology. Algebraic Methodology and Software Technology, Lect. Notes Comput. Sci., vol. 1101 (1996), Springer), 117-131
[41] Kapur, D.; Zhang, H., RRL: a rewrite rule laboratory, (Lusk, E.; Overbeek, R., 9th International Conference on Automated Deduction. 9th International Conference on Automated Deduction, Lect. Notes Comput. Sci., vol. 310 (1988), Springer: Springer Berlin/Heidelberg), 768-769
[42] Kounalis, E.; Rusinowitch, M., Mechanizing inductive reasoning, (Proceedings of the Eighth National Conference on Artificial Intelligence, vol. 1. Proceedings of the Eighth National Conference on Artificial Intelligence, vol. 1, AAAI’90 (1990), AAAI Press), 240-245 · Zbl 0744.68114
[43] Lescanne, P., Computer experiments with the REVE term rewriting system generator, (Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’83 (1983), ACM: ACM New York, NY, USA), 99-108
[44] Lescanne, P., Implementation of completion by transition rules + control: ORME, (Kirchner, H.; Wechler, W., Algebraic and Logic Programming. Algebraic and Logic Programming, Lect. Notes Comput. Sci., vol. 463 (1990), Springer: Springer Berlin/Heidelberg), 262-269
[45] Liu, P.; Chang, R.-J., A new structural induction scheme for proving properties of mutually recursive concepts, (6th National Conference on Artificial Intelligence, vol. 1 (1987), AAAI Press), 144-148
[46] Musser, D. R., On proving inductive properties of abstract data types, (POPL (1980)), 154-162
[47] Nieuwenhuis, R.; Rubio, A., Paramodulation-based theorem proving, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning (2001), Elsevier and MIT Press), 371-443 · Zbl 0997.03012
[48] Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL — A Proof Assistant for Higher-Order Logic, Lect. Notes Comput. Sci., vol. 2283 (2002), Springer · Zbl 0994.68131
[49] Protzen, M., Lazy generation of induction hypotheses, (Automated Deduction—CADE-12 (1994)), 42-56 · Zbl 1433.68563
[50] Reddy, U., Term rewriting induction, (Proceedings of the 10th International Conference on Automated Deduction (1990)), 162-177 · Zbl 1509.68123
[51] Rusinowitch, M.; Stratulat, S.; Klay, F., Mechanical verification of an ideal incremental ABR conformance algorithm, J. Autom. Reason., 30, 2, 53-177 (2003) · Zbl 1023.68090
[52] Sozeau, M., Program-ing finger trees in Coq, (Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming. Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP ’07 (2007), ACM: ACM New York, NY, USA), 13-24 · Zbl 1291.68157
[53] Sozeau, M., Equations: a dependent pattern-matching compiler, (Kaufmann, M.; Paulson, L. C., Interactive Theorem Proving, First International Conference, Proceedings. Interactive Theorem Proving, First International Conference, Proceedings, ITP 2010, Edinburgh, UK, July 11-14, 2010. Interactive Theorem Proving, First International Conference, Proceedings. Interactive Theorem Proving, First International Conference, Proceedings, ITP 2010, Edinburgh, UK, July 11-14, 2010, Lect. Notes Comput. Sci., vol. 6172 (2010), Springer), 419-434 · Zbl 1291.68369
[54] Stratulat, S., Preuves par récurrence avec ensembles couvrants contextuels. applications à la vérification de logiciels de télécommunications (2012), Université Henri Poincaré, Nancy I: Editions Universitaires Européennes, Also published as a book at
[55] Stratulat, S., A general framework to build contextual cover set induction provers, J. Symb. Comput., 32, 4, 403-445 (2001) · Zbl 0981.68147
[56] Stratulat, S., Combining rewriting with Noetherian induction to reason on non-orientable equalities, (Voronkov, A., Rewriting Techniques and Applications. Rewriting Techniques and Applications, Lect. Notes Comput. Sci., vol. 5117 (2008), Springer: Springer Berlin), 351-365 · Zbl 1145.68454
[57] Stratulat, S., Integrating implicit induction proofs into certified proof environments, (IFM’2010 (8th International Conference on Integrated Formal Methods). IFM’2010 (8th International Conference on Integrated Formal Methods), Lect. Notes Comput. Sci., vol. 6396 (2010)), 320-335
[58] Stratulat, S., A unified view of induction reasoning for first-order logic, (Voronkov, A., Turing-100 (The Alan Turing Centenary Conference). Turing-100 (The Alan Turing Centenary Conference), Epic Ser., vol. 10 (2012), EasyChair), 326-352
[59] Stratulat, S., Implementing reasoning modules in implicit induction theorem provers, (SYNASC (International Symposium on Symbolic and Numeric Algorithms for Scientific Computing) (2014), IEEE), 133-140
[60] Stratulat, S.; Demange, V., Automated certification of implicit induction proofs, (CPP’2011 (First International Conference on Certified Programs and Proofs). CPP’2011 (First International Conference on Certified Programs and Proofs), Lect. Notes Comput. Sci., vol. 7086 (2011), Springer Verlag), 37-53 · Zbl 1350.68245
[61] The CompCert project (2014)
[62] The Coq development team, The Coq Reference Manual - version 8.4. INRIA (2013)
[63] The Flyspeck website (2014)
[64] The L4.verified project (2014)
[65] The SPIKE development team, The SPIKE prover (2014)
[67] Walther, C., Combining induction axioms by machine, (Bajcsy, R., IJCAI - Proceedings of the 13th International Joint Conference on Artificial Intelligence. IJCAI - Proceedings of the 13th International Joint Conference on Artificial Intelligence, Chambéry, France, August 28-September 3 (1993)), 95-101 (1993), Morgan Kaufmann
[68] Wirth, C.-P., Descente infinie + deduction, Log. J. IGPL, 12, 1, 1-96 (2004) · Zbl 1067.03021
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.