×

Inductive theorem proving based on tree grammars. (English) Zbl 1386.03018

Summary: Induction plays a key role in reasoning in many areas of mathematics and computer science. A central problem in the automation of proof by induction is the non-analytic nature of induction invariants. In this paper we present an algorithm for proving universal statements by induction that separates this problem into two phases. The first phase consists of a structural analysis of witness terms of instances of the universal statement. The result of such an analysis is a tree grammar which induces a quantifier-free unification problem which is solved in the second phase. Each solution to this problem is an induction invariant. The arguments and techniques used in this paper heavily exploit a correspondence between tree grammars and proofs already applied successfully to the generation of non-analytic cuts in the setting of pure first-order logic.

MSC:

03B35 Mechanization of proofs and logical operations
03F07 Structure of proofs
03F03 Proof theory in general (including proof-theoretic semantics)
03F30 First-order arithmetic and fragments
68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Armando, Alessandro; Rusinowitch, Michaël; Stratulat, Sorin, Incorporating decision procedures in implicit induction, J. Symbolic Comput., 34, 4, 241-258 (2002) · Zbl 1037.68129
[2] Baader, Franz; Nipkow, Tobias, Term Rewriting and All That (1998), Cambridge University Press · Zbl 0948.68098
[3] Baker, Siani; Ireland, Andrew; Smaill, Alan, On the use of the constructive omega-rule within automated deduction, (Voronkov, Andrei, Logic Programming and Automated Reasoning. Logic Programming and Automated Reasoning, LPAR, 1992. Logic Programming and Automated Reasoning. Logic Programming and Automated Reasoning, LPAR, 1992, Lecture Notes in Computer Science, vol. 624 (1992)), 214-225 · Zbl 0920.03018
[4] Biere, Armin; Cimatti, Alessandro; Clarke, Edmund M.; Zhu, Yunshan, Symbolic model checking without BDDs, (Cleaveland, Rance, Tools and Algorithms for Construction and Analysis of Systems. Tools and Algorithms for Construction and Analysis of Systems, TACAS, 1999. Tools and Algorithms for Construction and Analysis of Systems. Tools and Algorithms for Construction and Analysis of Systems, TACAS, 1999, Lecture Notes in Computer Science, vol. 1579 (1999), Springer), 193-207
[5] Bradley, Aaron R.; Manna, Zohar, The Calculus of Computation (2007), Springer · Zbl 1126.03001
[6] Brotherston, James; Gorogiannis, Nikos; Petersen, Rasmus L., A generic cyclic theorem prover, (Proceedings of APLAS-10. Proceedings of APLAS-10, Lecture Notes in Computer Science (2012), Springer), 350-367
[7] Brotherston, James; Simpson, Alex, Sequent calculi for induction and infinite descent, J. Logic Comput., 21, 6, 1177-1216 (2011) · Zbl 1242.03084
[8] Bundy, Alan, The automation of proof by mathematical induction, (Voronkov, Andrei; Robinson, John Alan, Handbook of Automated Reasoning, vol. 1 (2001), Elsevier), 845-911 · Zbl 0994.03007
[9] Bundy, Alan; Basin, David; Hutter, Dieter; Ireland, Andrew, Rippling: Meta-Level Guidance for Mathematical Reasoning, Cambridge Tracts in Theoretical Computer Science (2005), Cambridge University Press · Zbl 1095.68108
[10] Comon, H.; Dauchet, M.; Gilleron, R.; Löding, C.; Jacquemard, F.; Lugiez, D.; Tison, S.; Tommasi, M., Tree automata techniques and applications (2007), release October, 12th 2007
[11] De Moura, Leonardo; Bjørner, Nikolaj, Satisfiability modulo theories: introduction and applications, Commun. ACM, 54, 9, 69-77 (2011)
[12] Eberhard, Sebastian; Hetzl, Stefan, Algorithmic compression of finite tree languages by rigid acyclic grammars, Preprint available at: · Zbl 1390.68388
[13] Eberhard, Sebastian; Hetzl, Stefan, Undecidability results for simple induction proofs, Preprint available at: · Zbl 1390.68389
[14] Gécseg, Ferenc; Steinby, Magnus, Tree languages, (Rozenberg, G.; Salomaa, A., Beyond Words. Beyond Words, Handbook of Formal Languages, vol. 3 (1997), Springer), 1-68 · Zbl 1499.68177
[15] Gentzen, Gerhard, Untersuchungen über das logische Schliessen, Math. Z., 39, 1, 176-210 (1935) · Zbl 0010.14501
[16] Gentzen, Gerhard, Die Widerspruchsfreiheit der reinen Zahlentheorie, Math. Ann., 112, 493-565 (1936) · JFM 62.0044.01
[17] Heras, Federico; Larrosa, Javier; Oliveras, Albert, Minimaxsat: a new weighted max-sat solver, (International Conference on Theory and Applications of Satisfiability Testing (2007), Addison-Wesley), 41-55
[18] Herbrand, Jacques, Recherches sur la théorie de la démonstration (1930), Université de Paris, PhD thesis · JFM 56.0824.02
[19] Hetzl, Stefan, Applying tree languages in proof theory, (Dediu, Adrian-Horia; Martín-Vide, Carlos, Language and Automata Theory and Applications. Language and Automata Theory and Applications, LATA, 2012. Language and Automata Theory and Applications. Language and Automata Theory and Applications, LATA, 2012, Lecture Notes in Computer Science, vol. 7183 (2012), Springer) · Zbl 1350.68170
[20] Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Tapolczai, Janos; Weller, Daniel, Introducing quantified cuts in logic with equality, (Demri, Stéphane; Kapur, Deepak; Weidenbach, Christoph, Automated Reasoning - 7th International Joint Conference. Automated Reasoning - 7th International Joint Conference, IJCAR. Automated Reasoning - 7th International Joint Conference. Automated Reasoning - 7th International Joint Conference, IJCAR, Lecture Notes in Computer Science, vol. 8562 (2014), Springer), 240-254 · Zbl 1423.68418
[21] Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel, Algorithmic introduction of quantified cuts, Theoret. Comput. Sci., 549, 1-16 (2014) · Zbl 1393.03050
[22] Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel, Towards algorithmic cut-introduction, (Logic for Programming, Artificial Intelligence and Reasoning. Logic for Programming, Artificial Intelligence and Reasoning, LPAR-18. Logic for Programming, Artificial Intelligence and Reasoning. Logic for Programming, Artificial Intelligence and Reasoning, LPAR-18, Lecture Notes in Computer Science, vol. 7180 (2012), Springer), 228-242 · Zbl 1352.68213
[23] Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Paleo, Bruno Woltzenlogel, Herbrand sequent extraction, (Autexier, Serge; Campbell, John; Rubio, Julio; Sorge, Volker; Suzuki, Masakazu; Wiedijk, Freek, Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Artificial Intelligence, vol. 5144 (2008), Springer), 462-477 · Zbl 1166.68347
[24] Hetzl, Stefan; Straßburger, Lutz, Herbrand-confluence for cut-elimination in classical first-order logic, (Cégielski, Patrick; Durand, Arnaud, Computer Science Logic. Computer Science Logic, CSL, 2012. Computer Science Logic. Computer Science Logic, CSL, 2012, Leibniz International Proceedings in Informatics (LIPIcs), vol. 16 (2012), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik), 320-334 · Zbl 1252.03123
[25] Jacquemard, Florent; Klay, Francis; Vacher, Camille, Rigid tree automata, (Dediu, Adrian Horia; Ionescu, Armand-Mihai; Martín-Vide, Carlos, Language and Automata Theory and Applications. Language and Automata Theory and Applications, LATA, 2009. Language and Automata Theory and Applications. Language and Automata Theory and Applications, LATA, 2009, Lecture Notes in Computer Science, vol. 5457 (2009), Springer), 446-457 · Zbl 1234.68213
[26] Jacquemard, Florent; Klay, Francis; Vacher, Camille, Rigid tree automata and applications, Inform. and Comput., 209, 486-512 (2011) · Zbl 1217.68131
[27] Johansson, Moa; Dixon, Lucas; Bundy, Alan, Conjecture synthesis for inductive theories, J. Automat. Reason., 47, 3, 251-289 (2011) · Zbl 1243.68268
[28] (Kaufmann, Matt; Manolios, Panagiotis; Moore, J. Strother, Computer-Aided Reasoning: ACL2 Case Studies (2000), Kluwer Academic Publishers)
[29] Kaufmann, Matt; Manolios, Panagiotis; Moore, J. Strother, Computer-Aided Reasoning: An Approach (2000), Kluwer Academic Publishers
[30] Claessen, Koen; Johansson, Moa; Rosén, Dan; Smallbone, Nicholas, Automating inductive proofs using theory exploration, (Bonacina, Maria Paola, Proceedings of the 24th International Conference on Automated Deduction. Proceedings of the 24th International Conference on Automated Deduction, CADE-24. Proceedings of the 24th International Conference on Automated Deduction. Proceedings of the 24th International Conference on Automated Deduction, CADE-24, Lecture Notes in Computer Science, vol. 7898 (2013), Springer), 392-406 · Zbl 1381.68263
[31] Sonnex, William; Drossopoulou, Sophia; Eisenbach, Susan, Zeno: an automated prover for properties of recursive data structures, (Flanagan, Cormac; König, Barbara, The 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. The 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2012. The 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. The 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2012, Lecture Notes in Computer Science, vol. 7214 (2012), Springer), 407-421 · Zbl 1352.68216
[32] Sutcliffe, G., The TPTP world - infrastructure for automated reasoning, (Clarke, E.; Voronkov, A., Proceedings of the 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning. Proceedings of the 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Lecture Notes in Artificial Intelligence, vol. 6355 (2010), Springer-Verlag), 1-12 · Zbl 1253.68292
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.