On the generation of quantified lemmas. (English) Zbl 1459.03011
Summary: In this paper we present an algorithmic method of lemma introduction. Given a proof in predicate logic with equality the algorithm is capable of introducing several universal lemmas. The method is based on an inversion of Gentzen’s cut-elimination method for sequent calculus. The first step consists of the computation of a compact representation (a so-called decomposition) of Herbrand instances in a cut-free proof. Given a decomposition the problem of computing the corresponding lemmas is reduced to the solution of a second-order unification problem (the solution conditions). It is shown that that there is always a solution of the solution conditions, the canonical solution. This solution yields a sequence of lemmas and, finally, a proof based on these lemmas. Various techniques are developed to simplify the canonical solution resulting in a reduction of proof complexity. Moreover, the paper contains a comprehensive empirical evaluation of the implemented method and gives an application to a mathematical proof.
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 03F05 | Cut-elimination and normal-form theorems |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Afshari, B., Hetzl, S., Leigh, G.E.: Herbrand disjunctions, cut elimination and context-free tree grammars. In: Altenkirch, T., (ed.) International Conference on Typed Lambda Calculi and Applications (TLCA) 2015, LIPIcs, vol. 38, pp. 1-16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015) · Zbl 1366.03235 |
| [2] | Afshari, B.; Hetzl, S.; Leigh, GE; Probst, D. (ed.); Schuster, P. (ed.), Herbrand confluence for first-order proofs with \[\Pi_2\] Π2-cuts, 5-40 (2016), Berlin · Zbl 1433.03133 |
| [3] | Afshari, B., Hetzl, S., Leigh, G.E.: On the Herbrand content of LK. In: Kohlenbach, U., van Bakel, S., Berardi,S., (eds.) 6th International Workshop on Classical Logic and Computation (CL&C 2016), EPTCS, vol. 213, pp. 1-10 (2016) · Zbl 1482.03014 |
| [4] | Afshari, B., Hetzl, S., Leigh G.E.: Herbrand’s Theorem as Higher-Order Recursion. Preprint OWP-2018-01, Mathematisches Forschungsinstitut Oberwolfach (2018) · Zbl 1464.03085 |
| [5] | Baaz, M., Zach, R.: Algorithmic structuring of cut-free proofs. In: Computer Science Logic (CSL) 1992. Lecture Notes in Computer Science, vol. 702, pp. 29-42. Springer (1993) · Zbl 0794.03076 |
| [6] | Birkhoff, G.: Lattice Theory, American Mathematical Society Colloquium Publications, vol. XXV, 3rd edn. American Mathematical Society, Providence (1967) · Zbl 0126.03801 |
| [7] | Bundy, A.; Voronkov, A. (ed.); Robinson, JA (ed.), The automation of proof by mathematical induction, 845-911 (2001), Amsterdam · Zbl 0994.03007 · doi:10.1016/B978-044450813-3/50015-1 |
| [8] | Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning, Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2005) · Zbl 1095.68108 · doi:10.1017/CBO9780511543326 |
| [9] | Cavagnetto, S.: The lengths of proofs: Kreisel’s conjecture and Gödels speed-up theorem. J. Math. Sci. 158(5), 689-707 (2009) · Zbl 1207.03071 · doi:10.1007/s10958-009-9408-0 |
| [10] | Colton, S.: Automated theory formation in pure mathematics. Ph.D. thesis, University of Edinburgh (2001) · Zbl 1219.68141 |
| [11] | Colton, S.: Automated Theory Formation in Pure Mathematics. Springer, Berlin (2002) · Zbl 1219.68141 · doi:10.1007/978-1-4471-0147-5 |
| [12] | Eberhard, S., Ebner, G., Hetzl, S.: Algorithmic compression of finite tree languages by rigid acyclic grammars. ACM Trans. Comput. Log. 18(4), 26:1-26:20 (2017) · Zbl 1407.68251 · doi:10.1145/3127401 |
| [13] | Eberhard, S., Hetzl, S.: Inductive theorem proving based on tree grammars. Ann. Pure Appl. Log. 166(6), 665-700 (2015) · Zbl 1386.03018 · doi:10.1016/j.apal.2015.01.002 |
| [14] | Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: GAPT 2.0. In: 8th International Joint Conference on Automated Reasoning, IJCAR (2016) · Zbl 1475.68433 |
| [15] | Finger, M., Gabbay, D.: Equal rights for the cut: computable non-analytic cuts in cut-based proofs. Log. J. IGPL 15(5-6), 553-575 (2007) · Zbl 1159.03038 · doi:10.1093/jigpal/jzm040 |
| [16] | Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39, 176-210,405-431 (1934-1935) · Zbl 0010.14601 |
| [17] | Hetzl, S., Leitsch, A., Reis, G., Tapolczai, J., Weller, D.: Introducing quantified cuts in logic with equality. In: Demri, S., Kapur, D., Weidenbach, C., (eds.) Automated Reasoning - 7th International Joint Conference, IJCAR. Lecture Notes in Computer Science, vol. 8562, pp. 240-254. Springer (2014) · Zbl 1423.68418 |
| [18] | Hetzl, S., Leitsch, A., Reis, G., Weller, D.: Algorithmic introduction of quantified cuts. Theor. Comput. Sci. 549, 1-16 (2014) · Zbl 1393.03050 · doi:10.1016/j.tcs.2014.05.018 |
| [19] | Hetzl, S., Leitsch, A., Weller, D.: Towards algorithmic cut-introduction. In: Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18). Lecture Notes in Computer Science, vol. 7180, pp. 228-242. Springer (2012) · Zbl 1352.68213 |
| [20] | Ireland, A., Bundy, A.: Productive use of failure in inductive proof. J. Autom. Reason. 16(1-2), 79-111 (1996) · Zbl 0847.68103 · doi:10.1007/BF00244460 |
| [21] | Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. J. Autom. Reason. 47(3), 251-289 (2011) · Zbl 1243.68268 · doi:10.1007/s10817-010-9193-y |
| [22] | Leitsch, A., Lettmann, M.P.: The problem of \[\Pi_2\] Π2-cut-introduction. Theor. Comput. Sci. 706, 83-116 (2018) · Zbl 1423.03240 · doi:10.1016/j.tcs.2017.10.003 |
| [23] | Miller, D., Nigam, V.: Incorporating tables into proofs. In: 16th Conference on Computer Science and Logic (CSL07). Lecture Notes in Computer Science, vol. 4646, pp. 466-480. Springer (2007) · Zbl 1179.03019 |
| [24] | Orevkov, V.: Lower bounds for increasing complexity of derivations after cut elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta 88, 137-161 (1979) · Zbl 0429.03033 |
| [25] | Plotkin, G.D.: A note on inductive generalization. Mach. Intell. 5(1), 153-163 (1970) · Zbl 0219.68045 |
| [26] | Plotkin, G.D.: A further note on inductive generalization. Mach. Intell. 6, 101-124 (1971) · Zbl 0261.68042 |
| [27] | Pudlák, P.; Buss, S. (ed.), The Lengths of Proofs, 547-637 (1998), Amsterdam · Zbl 0920.03056 · doi:10.1016/S0049-237X(98)80023-2 |
| [28] | Reynolds, J.C.: Transformational systems and the algebraic structure of atomic formulas. Mach. Intell. 5(1), 135-151 (1970) · Zbl 0219.68044 |
| [29] | Shoenfield, J.R.: Mathematical Logic, 2nd edn. Addison Wesley, Boston (1973) · Zbl 0965.03001 |
| [30] | Sorge, V., Colton, S., McCasland, R., Meier, A.: Classification results in quasigroup and loop theory via a combination of automated reasoning tools. Comment. Math. Univ. Carol. 49(2), 319-339 (2008) · Zbl 1192.20062 |
| [31] | Sorge, V., Meier, A., McCasland, R., Colton, S.: Automatic construction and verification of isotopy invariants. J. Autom. Reason. 40(2-3), 221-243 (2008) · Zbl 1139.68050 · doi:10.1007/s10817-007-9093-y |
| [32] | Statman, R.: Lower bounds on Herbrand’s theorem. Proc. Am. Math. Soc. 75, 104-107 (1979) · Zbl 0411.03048 |
| [33] | Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337-362 (2009) · Zbl 1185.68636 · doi:10.1007/s10817-009-9143-8 |
| [34] | Vyskočil, J., Stanovský, D., Urban, J.: Automated proof compression by invention of new definitions. In: Clark, E.M., Voronkov, A., (eds.) Logic for Programming, Artifical Intelligence and Reasoning (LPAR-16). Lecture Notes in Computer Science, vol. 6355, pp. 447-462. Springer (2010) · Zbl 1203.68004 |
| [35] | Woltzenlogel Paleo, B.: Atomic cut introduction by resolution: proof structuring and compression. In: Clark, E.M., Voronkov, A., (eds.) Logic for Programming, Artifical Intelligence and Reasoning (LPAR-16). Lecture Notes in Computer Science, vol. 6355, pp. 463-480. Springer (2010) · Zbl 1253.03085 |
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.
