Lemmatization for stronger reasoning in large theories. (English) Zbl 1471.68313

Lutz, Carsten (ed.) et al., Frontiers of combining systems. 10th international symposium, FroCoS 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9322, 341-356 (2015).
Summary: In this work we improve ATP performance in large theories by the reuse of lemmas derived in previous related problems. Given a large set of related problems to solve, we run automated theorem provers on them, extract a large number of lemmas from the proofs found and post-process the lemmas to make them usable in the remaining problems. Then we filter the lemmas by several tools and extract their proof dependencies, and use machine learning on such proof dependencies to add the most promising generated lemmas to the remaining problems. On such enriched problems we run the automated provers again, solving more problems. We describe this method and the techniques we used, and measure the improvement obtained. On the MPTP2078 large-theory benchmark the method yields 6.6% and 6.2% more problems proved in two different evaluation modes.
For the entire collection see [Zbl 1355.68017].


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68T05 Learning and adaptive systems in artificial intelligence
Full Text: DOI Link


[1] Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning 52(2), 191–213 (2014) · Zbl 1315.68217
[2] Blanchette, J.C.: Redirecting proofs by contradiction. In: Blanchette, J.C., Urban, J. (eds.) PxTP@CADE. EPiC Series, vol. 14, pp. 11–26. EasyChair (2013)
[3] Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning (in press, 2015)
[4] Fiedler, A.: P.rex: An interactive proof explainer. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 416–420. Springer, Heidelberg (2001) · Zbl 0988.68596
[5] Kaliszyk, C., Urban, J.: Stronger automation for Flyspeck by feature weighting and strategy evolution. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013. EPiC Series, vol. 14, pp. 87–95. EasyChair (2013)
[6] Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning 53(2), 173–213 (2014) · Zbl 1314.68283
[7] Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. Journal of Symbolic Computation 69, 109–128 (2015) · Zbl 1315.68220
[8] Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Automated Reasoning (in press, 2015) · Zbl 1356.68191
[9] Kinyon, M., Veroff, R., Vojtěchovský, P.: Loops with abelian inner mapping groups: An application of automated deduction. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 151–164. Springer, Heidelberg (2013) · Zbl 1383.68077
[10] Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013) · Zbl 06233023
[11] Kuehlwein, D., Urban, J.: Learning from multiple proofs: First experiments. In: Fontaine, P., Schmidt, R.A., Schulz, S. (eds.) PAAR 2012. EPiC Series, vol. 21, pp. 82–94. EasyChair (2013)
[12] Kühlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: Machine learning for sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35–50. Springer, Heidelberg (2013) · Zbl 1317.68215
[13] Meier, A.: System description: Tramp: transformation of machine-found proofs into nd-proofs at the assertion level. In: McAllester, D. (ed.) CADE 2000. LNCS(LNAI), vol. 1831, pp. 460–464. Springer, Heidelberg (2000) · Zbl 0963.68537
[14] Page, L., Brin, S., Motwani, R., Winograd, T.: The PageRank citation ranking: Bringing order to the Web. Technical report, Stanford Digital Library Technologies Project (1998)
[15] Phillips, J.D., Stanovský, D.: Automated theorem proving in quasigroup and loop theory. AI Commun. 23(2–3), 267–283 (2010) · Zbl 1204.68181
[16] Puzis, Y., Gao, Y., Sutcliffe, G.: Automated generation of interesting theorems. In: Sutcliffe, G., Goebel, R. (eds.) FLAIRS, pp. 49–54. AAAI Press (2006)
[17] Schulz, S.: Learning search control knowledge for equational deduction. DISKI, vol. 230. Infix Akademische Verlagsgesellschaft (2000) · Zbl 0994.68130
[18] Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013) · Zbl 1407.68442
[19] Smolka, S.J., Blanchette, J.C.: Robust, semi-intelligible Isabelle proofs from ATP proofs. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013. EPiC Series, vol. 14, pp. 117–132. EasyChair (2013)
[20] Sutcliffe, G., Puzis, Y.: SRASS - A semantic relevance axiom selection system. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 295–310. Springer, Heidelberg (2007) · Zbl 1213.68575
[21] Urban, J.: MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. on Artificial Intelligence Tools 15(1), 109–130 (2006) · Zbl 05421611
[22] Urban, J.: BliStr: The Blind Strategymaker. CoRR, abs/1301.2683 (2014) (accepted to PAAR 2014)
[23] Urban, J., Sutcliffe, G.: ATP-based cross-verification of Mizar proofs: Method, systems, and first experiments. MCS 2(2), 231–251 (2008) · Zbl 1178.68532
[24] Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, J.: MaLARea SG1 - machine learner for automated reasoning with semantic guidance. In: IJCAR, pp. 441–456 (2008) · Zbl 1165.68434
[25] Urban, J., Sutcliffe, G., Trac, S., Puzis, Y.: Combining mizar and TPTP semantic presentation and verification Tools. Studies in Logic, Grammar and Rhetoric 18(31), 121–136 (2009)
[26] Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: Case studies. J. Autom. Reasoning 16(3), 223–239 (1996) · Zbl 0857.68095
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.