Induction and Skolemization in saturation theorem proving. (English) Zbl 07601550
Summary: We consider a typical integration of induction in saturation-based theorem provers and investigate the effects of Skolem symbols occurring in the induction formulas. In a practically relevant setting we establish a Skolem-free characterization of refutation in saturation-based proof systems with induction. Finally, we use this characterization to obtain unprovability results for a concrete saturation-based induction prover.
MSC:
| 03F30 | First-order arithmetic and fragments |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 03B70 | Logic in computer science |
| 03H15 | Nonstandard models of arithmetic |
Keywords:
inductive theorem proving; weak arithmetical theories; skolemization; saturation theorem provingReferences:
| [1] | Adamowicz, Zofia, Parameter-free induction, the Matiyasevič theorem and \(B \operatorname{\Sigma}_1\), (Drake, F. R.; Truss, J. K., Logic Colloquium ’86. Logic Colloquium ’86, Studies in Logic and the Foundations of Mathematics, vol. 124 (1987), Elsevier), 1-8 |
| [2] | Beklemishev, Lev D., Parameter free induction and reflection, (Gottlob, Georg; Leitsch, Alexander; Mundici, Daniele, Computational Logic and Proof Theory. Computational Logic and Proof Theory, Lecture Notes in Computer Science, vol. 1289 (1997), Springer), 103-113 · Zbl 0892.03023 |
| [3] | Beklemishev, Lev D., Quantifier-free induction schema and the least element principle, Proc. Steklov Inst. Math., 242, 50-67 (2003) · Zbl 1079.03049 |
| [4] | Brotherston, James; Gorogiannis, Nikos; Lerchedahl Petersen, Rasmus, A generic cyclic theorem prover, (Jhala, Ranjit; Igarashi, Atsushi, Programming Languages and Systems. Programming Languages and Systems, Lecture Notes in Computer Science, vol. 7705 (2012), Springer), 350-367 |
| [5] | Biundo, Susanne; Hummel, Birgit; Hutter, Dieter; Walther, Christoph, The Karlsruhe induction theorem proving system, (Siekmann, Jörg H., 8th International Conference on Automated Deduction. 8th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 230 (1986), Springer), 672-674 |
| [6] | Baaz, Matthias; Hetzl, Stefan; Weller, Daniel, On the complexity of proof deskolemization, J. Symb. Log., 77, 2, 669-686 (2012) · Zbl 1345.03104 |
| [7] | Baaz, Matthias; Leitsch, Alexander, On Skolemization and proof complexity, Fundam. Inform., 20, 4, 353-379 (1994) · Zbl 0815.03003 |
| [8] | Boyer, Robert S.; Moore, J. Strother, A Computational Logic, ACM Monograph Series (1979), Academic Press: Academic Press New York, Edited by Thomas A. Standish · Zbl 0448.68020 |
| [9] | Brotherston, James, Cyclic proofs for first-order logic with inductive definitions, (Beckert, Bernhard, Automated Reasoning with Analytic Tableaux and Related Methods. Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Computer Science, vol. 3702 (2005), Springer), 78-92 · Zbl 1142.03366 |
| [10] | Bundy, Alan; Stevens, Andrew; van Harmelen, Frank; Ireland, Andrew; Rippling, Alan Smaill, A heuristic for guiding inductive proofs, Artif. Intell., 62, 2, 185-253 (1993) · Zbl 0789.68121 |
| [11] | Berardi, Stefano; Tatsuta, Makoto, Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system, (Esparza, Javier; Murawski, Andrzej S., Foundations of Software Science and Computation Structures. Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, vol. 10203 (2017), Springer), 301-317 · Zbl 1486.03094 |
| [12] | Berardi, Stefano; Tatsuta, Makoto, Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proofs, Log. Methods Comput. Sci., 15, 3 (August 2019) · Zbl 1509.03158 |
| [13] | Bundy, Alan; van Harmelen, Frank; Hesketh, Jane; Smaill, Alan; Stevens, Andrew, A rational reconstruction and extension of recursion analysis, (Sridharan, N. S., Proceedings of the 11th International Joint Conference on Artificial Intelligence. Proceedings of the 11th International Joint Conference on Artificial Intelligence, Detroit, MI, USA, August 1989 (1989), Morgan Kaufmann), 359-365 · Zbl 0708.68061 |
| [14] | Cordón-Franco, Andrés; Fernández-Margarit, Alejandro; Félix Lara Martín, Francisco, A note on parameter free \(\operatorname{\Pi}_1\)-induction and restricted exponentiation, Math. Log. Q., 57, 5, 444-455 (2011) · Zbl 1238.03048 |
| [15] | Claessen, Koen; Johansson, Moa; Rosén, Dan; Smallbone, Nicholas, Automating inductive proofs using theory exploration, (Paola Bonacina, Maria, Automated Deduction - CADE-24. Automated Deduction - CADE-24, Lecture Notes in Computer Science, vol. 7898 (2013), Springer), 392-406 · Zbl 1381.68263 |
| [16] | Claessen, Koen; Johansson, Moa; Rosén, Dan; Smallbone, Nicholas, TIP: Tons of inductive problems, (Kerber, Manfred; Carette, Jacques; Kaliszyk, Cezary; Rabe, Florian; Sorge, Volker, Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 9150 (2015), Springer), 333-337 · Zbl 1417.68179 |
| [17] | Comon, Hubert, Inductionless induction, (Robinson, Alan; Voronkov, Andrei, Handbook of Automated Reasoning, vol. 1 (2001), North-Holland: North-Holland Amsterdam), 913-962, chapter 14 · Zbl 0994.03006 |
| [18] | Cruanes, Simon, Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond (September 2015), École Polytechnique: École Polytechnique Palaiseau, France, PhD thesis |
| [19] | Cruanes, Simon, Superposition with structural induction, (Dixon, Clare; Finger, Marcelo, Frontiers of Combining Systems. Frontiers of Combining Systems, Lecture Notes in Computer Science, vol. 10483 (2017), Springer), 172-188 · Zbl 1496.68365 |
| [20] | Dowek, Gilles, Skolemization in simple type theory: the logical, the theoretical points of view, (Benzmüller, Christoph; Brown, Chad; Siekmann, Jörg; Statman, Richard, Reasoning in Simple Type Theory. Reasoning in Simple Type Theory, Studies in Logic, Mathematical Logic and Foundations (2008)), College Publications · Zbl 1226.03016 |
| [21] | Eberhard, Sebastian; Hetzl, Stefan, Inductive theorem proving based on tree grammars, Ann. Pure Appl. Log., 166, 6, 665-700 (2015) · Zbl 1386.03018 |
| [22] | Echenim, Mnacho; Peltier, Nicolas, Combining induction and saturation-based theorem proving, J. Autom. Reason., 64, 2, 253-294 (2020) · Zbl 1476.68300 |
| [23] | Hajdú, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei, Induction with generalization in superposition reasoning, (Benzmüller, Christoph; Miller, Bruce R., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 12236 (2020), Springer), 123-137 · Zbl 1455.68248 |
| [24] | Hetzl, Stefan; Vierling, Jannik, Clause set cycles and induction, Log. Methods Comput. Sci., 16, 4, Article 11 pp. (November 2020) · Zbl 1516.03006 |
| [25] | Hetzl, Stefan; Lok Wong, Tin, Some observations on the logical foundations of inductive theorem proving, Log. Methods Comput. Sci., 13, 4 (April 2018) · Zbl 1460.03005 |
| [26] | Johansson, Moa; Dixon, Lucas; Bundy, Alan, IsaCoSy: synthesis of inductive theorems, (Workshop on Automated Mathematical Theory Exploration (Automatheo) (2009)) · Zbl 1243.68268 |
| [27] | Jeřábek, Emil, Induction rules in bounded arithmetic, Arch. Math. Log., 59, 3, 461-501 (2020) · Zbl 1471.03082 |
| [28] | Johansson, Moa; Rosén, Dan; Smallbone, Nicholas; Hipster, Koen Claessen, Integrating theory exploration in a proof assistant, (Watt, Stephen M.; Davenport, James H.; Sexton, Alan P.; Sojka, Petr; Urban, Josef, Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 8543 (2014), Springer), 108-122 · Zbl 1304.68157 |
| [29] | Kersani, Abdelkader, Preuves par induction dans le calcul de superposition (October 2014), Université de Grenoble, PhD thesis |
| [30] | Komara, Ján, Efficient elimination of Skolem functions in \(\text{LK}^{\text{h}} \), Arch. Math. Log. (Nov. 2021) |
| [31] | Kersani, Abdelkader; Peltier, Nicolas, Combining superposition and induction: a practical realization, (Fontaine, Pascal; Ringeissen, Christophe; Schmidt, Renate A., Frontiers of Combining Systems. Frontiers of Combining Systems, Lecture Notes in Computer Science, vol. 8152 (2013), Springer), 7-22 · Zbl 1398.68483 |
| [32] | Kaye, R.; Paris, J.; Dimitracopoulos, C., On parameter free induction schemas, J. Symb. Log., 53, 4, 1082-1097 (1988) · Zbl 0678.03025 |
| [33] | Dale, Miller, A compact representation of proofs, Stud. Log., 46, 4, 347-370 (1987) · Zbl 0644.03033 |
| [34] | Reddy, Uday S., Term rewriting induction, (Stickel, Mark E., 10th International Conference on Automated Deduction. 10th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 449 (1990), Springer), 162-177 · Zbl 1509.68123 |
| [35] | Reynolds, Andrew; Kuncak, Viktor, Induction for SMT solvers, (Deepak D’Souza; Lal, Akash; Larsen, Kim Guldstrand, Verification, Model Checking, and Abstract Interpretation. Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, vol. 8931 (2015), Springer), 80-98 · Zbl 1432.68418 |
| [36] | Reger, Giles; Voronkov, Andrei, Induction in saturation-based proof search, (Fontaine, Pascal, Automated Deduction - CADE 27. Automated Deduction - CADE 27, Lecture Notes in Computer Science, vol. 11716 (2019), Springer), 477-494 · Zbl 1535.68458 |
| [37] | Schmerl, Ulf R., Diophantine equations in fragments of arithmetic, Ann. Pure Appl. Log., 38, 2, 135-170 (1988) · Zbl 0661.03044 |
| [38] | Schoisswohl, Johannes, Automated induction by reflection (2020), Technische Universität Wien, Master’s thesis |
| [39] | Shepherdson, John C., A non-standard model for a free variable fragment of number theory, Bull. Acad. Pol. Sci., XII, 2, 79-86 (1964) · Zbl 0132.24701 |
| [40] | Shoenfield, Joseph R., Open sentences and the induction axiom, J. Symb. Log., 23, 1, 7-12 (1958) · Zbl 0085.24505 |
| [41] | Stevens, Andrew, A rational reconstruction of Boyer and Moore’s technique for constructing induction formulas, (Kodratoff, Yves, 8th European Conference on Artificial Intelligence, ECAI’88 (1988), Pitmann Publishing), 565-570 |
| [42] | Troelstra, Anne Sjerp; Schwichtenberg, Helmut, Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, vol. 43 (2000), Cambridge University Press · Zbl 0957.03053 |
| [43] | Vierling, Jannik, Cyclic superposition and induction (2018), Technische Universität Wien, Master’s thesis · Zbl 1516.03006 |
| [44] | Valbuena, Irene Lobo; Johansson, Moa, Conditional lemma discovery and recursion induction in Hipster, Electron. Commun. EASST, 72 (2015) |
| [45] | Voronkov, Andrei, AVATAR: the architecture for first-order theorem provers, (Biere, Armin; Bloem, Roderick, Computer Aided Verification. Computer Aided Verification, Lecture Notes in Computer Science, vol. 8559 (2014), Springer), 696-710 · Zbl 1495.68240 |
| [46] | Wand, Daniel, Superposition: Types and Induction (2017), Saarland University: Saarland University Saarbrücken, Germany, PhD thesis |
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.
