×

zbMATH — the first resource for mathematics

Aligning concepts across proof assistant libraries. (English) Zbl 1395.68247
Summary: As the knowledge available in the computer understandable proof corpora grows, recognizing repeating patterns becomes a necessary requirement in order to organize, synthesize, share, and transmit ideas. In this work, we automatically discover patterns in the libraries of interactive theorem provers and thus provide the basis for such applications for proof assistants. This involves detecting close properties, inducing the presence of matching concepts, as well as dynamically evaluating the quality of matches from the similarity of the environment of each concept. We further propose a classification process, which involves a disambiguation mechanism to decide which concepts actually represent the same mathematical ideas. We evaluate the approach on the libraries of six proof assistants based on different logical foundations: HOL4, HOL Light, and Isabelle/HOL for higher-order logic, Coq and Matita for intuitionistic type theory, and the Mizar Mathematical Library for set theory. Comparing the structures available in these libraries our algorithm automatically discovers hundreds of isomorphic concepts and thousands of highly similar ones.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Asperti, A.; Ricciotti, W.; Coen, C. S., Matita tutorial, J. Formal. Reason., 7, 2, 91-199, (2014)
[2] Aspinall, D.; Kaliszyk, C., Towards formal proof metrics, (Stevens, P.; Wasowski, A., 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016), Lect. Notes Comput. Sci., vol. 9633, (2016), Springer), 325-341
[3] Aspinall, D.; Kaliszyk, C., What’s in a theorem name? (rough diamond), (Blanchette, J.; Merz, S., 7th Conference on Interactive Theorem Proving (ITP 2016), Lect. Notes Comput. Sci., vol. 9807, (2016), Springer), 459-465 · Zbl 06644760
[4] Assaf, A.; Cauderlier, R., Mixing HOL and coq in dedukti (extended abstract), (Kaliszyk, C.; Paskevich, A., Proceedings Fourth Workshop on Proof eXchange for Theorem Proving (PxTP 2015), EPTCS, vol. 186, (2015)), 89-96
[5] Attal, S., Markov chains and dynamical systems: the open system point of view, Commun. Stoch. Anal., 4, 523-540, (2010) · Zbl 1331.82028
[6] Awodey, S., Category theory, Oxf. Log. Guides, vol. 49, (2006) · Zbl 1100.18001
[7] Bancerek, G.; Byliński, C.; Grabowski, A.; Korniłowicz, A.; Matuszewski, R.; Naumowicz, A.; Pąk, K.; Urban, J., Mizar: state-of-the-art and beyond, (Kerber, M.; Carette, J.; Kaliszyk, C.; Rabe, F.; Sorge, V., Intelligent Computer Mathematics - International Conference, CICM 2015, Lect. Notes Comput. Sci., vol. 9150, (2015), Springer), 261-279 · Zbl 1417.68201
[8] Barbarossa, M., Stability of discrete dynamical systems, Matrix, 21, a22, (2011)
[9] Blanchette, J. C.; Greenaway, D.; Kaliszyk, C.; Kühlwein, D.; Urban, J., A learning-based fact selector for isabelle/HOL, J. Autom. Reason., 57, 3, 219-244, (2016) · Zbl 1386.68149
[10] Blanqui, F., Rewriting modulo in deduction modulo, (Nieuwenhuis, R., Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Lect. Notes Comput. Sci., vol. 2706, (2003), Springer), 395-409 · Zbl 1038.68061
[11] Bortin, M.; Johnsen, E. B.; Lüth, C., Structured formal development in isabelle, Nord. J. Comput., 13, 1-2, 2-21, (2006) · Zbl 1114.68063
[12] Carlisle, D.; Davenport, J.; Dewar, M.; Hur, N.; Naylor, W., Conversion between mathml and openmath, (2001), The OpenMath Society, Tech. Rep. 24.969
[13] Corbineau, P.; Kaliszyk, C., Cooperative repositories for formal proofs, (Kauers, M.; Kerber, M.; Miner, R.; Windsteiger, W., Proc. of the 6th International Conference on Mathematical Knowledge Management (MKM’07), Lect. Notes Comput. Sci., vol. 4573, (2007), Springer), 221-234 · Zbl 1202.68377
[14] Corry, L., Modern algebra and the rise of mathematical structures, (2012), Birkhäuser
[15] Czajka, Ł.; Kaliszyk, C., Goal translation for a hammer for coq (extended abstract), (Blanchette, J.; Kaliszyk, C., Proceedings 1st International Workshop on Hammers for Type Theories (HaTT 2016), EPTCS, vol. 210, (2016)), 13-20
[16] Czajka, Ł.; Kaliszyk, C., Hammer for coq: automation for dependent type theory, J. Autom. Reason., (2018) · Zbl 1448.68458
[17] de Moura, L. M.; Kong, S.; Avigad, J., The Lean theorem prover (system description), (Felty, A. P.; Middeldorp, A., 25th International Conference on Automated Deduction (CADE), Lect. Notes Comput. Sci., vol. 9195, (2015), Springer), 378-388 · Zbl 06515520
[18] Dietrich, D.; Whiteside, I.; Aspinall, D., Polar: A framework for proof refactoring, (McMillan, K. L.; Middeldorp, A.; Voronkov, A., Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Lect. Notes Comput. Sci., vol. 8312, (2013), Springer), 776-791 · Zbl 1407.68434
[19] Dowek, G.; Hardin, T.; Kirchner, C., Theorem proving modulo, J. Autom. Reason., 31, 1, 33-72, (2003) · Zbl 1049.03011
[20] Gauthier, T.; Kaliszyk, C., Matching concepts across HOL libraries, (Watt, S.; Davenport, J.; Sexton, A.; Sojka, P.; Urban, J., Proc. of the 7th Conference on Intelligent Computer Mathematics (CICM’14), Lect. Notes Comput. Sci., vol. 8543, (2014), Springer), 267-281 · Zbl 1304.68154
[21] Gauthier, T.; Kaliszyk, C., Sharing HOL4 and HOL light proof knowledge, (Davis, M.; Fehnker, A.; McIver, A.; Voronkov, A., 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015), Lect. Notes Comput. Sci., vol. 9450, (2015), Springer), 372-386 · Zbl 06528794
[22] Gauthier, T.; Kaliszyk, C.; Urban, J., Initial experiments with statistical conjecturing over large formal corpora, (Kohlhase, A.; Libbrecht, P.; Miller, B. R.; Naumowicz, A.; Neuper, W.; Quaresma, P.; Tompa, F. W.; Suda, M., Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 (CICM-WiP 2016), CEUR, vol. 1785, (2016)), 219-228, CEUR-WS.org
[23] Grabowski, A.; Korniłowicz, A.; Naumowicz, A., Four decades of mizar, J. Autom. Reason., 55, 3, 191-198, (October 2015)
[24] Graf, P., Term indexing, Lect. Notes Comput. Sci., vol. 1053, (1996), Springer
[25] Haftmann, F.; Krauss, A.; Kunčar, O.; Nipkow, T., Data refinement in isabelle/HOL, (Blazy, S.; Paulin-Mohring, C.; Pichardie, D., Proc. of the 4th International Conference on Interactive Theorem Proving (ITP’13), Lect. Notes Comput. Sci., vol. 7998, (2013), Springer), 100-115 · Zbl 1317.68212
[26] Harrison, J., HOL light: an overview, (Berghofer, S.; Nipkow, T.; Urban, C.; Wenzel, M., TPHOLs, Lect. Notes Comput. Sci., vol. 5674, (2009), Springer), 60-66 · Zbl 1252.68255
[27] Harrison, J., The HOL light theory of Euclidean space, J. Autom. Reason., 50, 2, (2013), 173-190 · Zbl 1260.68373
[28] Harrison, J.; Urban, J.; Wiedijk, F., History of interactive theorem proving, (Siekmann, J. H., Computational Logic, Handb. Hist. Log., vol. 9, (2014), Elsevier), 135-214
[29] Hecht-Nielsen, R., Theory of the backpropagation neural network, Neural Netw., 1, Supplement-1, 445-448, (1988)
[30] Heras, J.; Komendantskaya, E., Recycling proof patterns in coq: case studies, Math. Comput. Sci., 8, 1, 99-116, (2014) · Zbl 1302.68243
[31] Hirsch, M. W., Stability and convergence in strongly monotone dynamical systems, J. Reine Angew. Math., 383, 1-53, (1988) · Zbl 0624.58017
[32] Huet, G.; Herbelin, H., 30 years of research and development around coq, (Jagannathan, S.; Sewell, P., Proc. 41st Symposium on Principles of Programming Languages (POPL’2014), (2014), ACM), 249-250 · Zbl 1284.68517
[33] Hurd, J., The opentheory standard theory library, (Bobaru, M. G.; Havelund, K.; Holzmann, G. J.; Joshi, R., NASA Formal Methods, Lect. Notes Comput. Sci., vol. 6617, (2011), Springer), 177-191
[34] Jacquel, M.; Berkani, K.; Delahaye, D.; Dubois, C., Verifying B proof rules using deep embedding and automated theorem proving, Softw. Syst. Model., 14, 1, 101-119, (2015)
[35] Jones, K. S., A statistical interpretation of term specificity and its application in retrieval, J. Doc., 28, 11-21, (1972)
[36] Kaliszyk, C.; Krauss, A., Scalable LCF-style proof translation, (Blazy, S.; Paulin-Mohring, C.; Pichardie, D., Proc. of the 4th International Conference on Interactive Theorem Proving (ITP’13), Lect. Notes Comput. Sci., vol. 7998, (2013), Springer), 51-66 · Zbl 1317.68214
[37] Kaliszyk, C.; Urban, J., Learning-assisted automated reasoning with flyspeck, J. Autom. Reason., 53, 2, 173-213, (2014) · Zbl 1314.68283
[38] Kaliszyk, C.; Urban, J., HOL(y)hammer: online ATP service for HOL light, Math. Comput. Sci., 9, 1, 5-22, (2015) · Zbl 1322.68177
[39] Kaliszyk, C.; Urban, J., Learning-assisted theorem proving with millions of lemmas, J. Symb. Comput., 69, 109-128, (2015) · Zbl 1315.68220
[40] Kaliszyk, C.; Urban, J.; Vyskočil, J.; Geuvers, H., Developing corpus-based translation methods between informal and formal mathematics, (Watt, S.; Davenport, J.; Sexton, A.; Sojka, P.; Urban, J., Proc. of the 7th Conference on Intelligent Computer Mathematics (CICM’14), Lect. Notes Comput. Sci., vol. 8543, (2014), Springer), 435-439 · Zbl 1304.68172
[41] Keller, C.; Werner, B., Importing HOL light into coq, (Kaufmann, M.; Paulson, L. C., ITP, Lect. Notes Comput. Sci., vol. 6172, (2010), Springer), 307-322 · Zbl 1291.68353
[42] Klein, G., Proof engineering considered essential, (Jones, C. B.; Pihlajasaari, P.; Sun, J., FM 2014: Formal Methods - 19th International Symposium, Lect. Notes Comput. Sci., vol. 8442, (2014), Springer), 16-21
[43] Landauer, T. K.; Foltz, P. W.; Laham, D., An introduction to latent semantic analysis, Discourse Process., 25, 2-3, 259-284, (1998)
[44] Meyer, B., Object-oriented software construction, vol. 2, (1988), Prentice hall New York
[45] Müller, D.; Gauthier, T.; Kaliszyk, C.; Kohlhase, M.; Rabe, F., Classification of alignments between concepts of formal mathematical systems, (Geuvers, H.; England, M.; Hasan, O.; Rabe, F.; Teschke, O., 10th International Conference on Intelligent Computer Mathematics (CICM’17), Lect. Notes Comput. Sci., vol. 10383, (2017), Springer), 83-98 · Zbl 1367.68309
[46] Myreen, M. O.; Davis, J., The reflective milawa theorem prover is sound - (down to the machine code that runs it), (Klein, G.; Gamboa, R., Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014. Proceedings, 2014, Vienna, Austria, July 14-17, 2014, Lect. Notes Comput. Sci., vol. 8558, (2014), Springer), 421-436 · Zbl 1416.68174
[47] Obua, S.; Skalberg, S., Importing HOL into isabelle/HOL, (Furbach, U.; Shankar, N., IJCAR, Lect. Notes Comput. Sci., vol. 4130, (2006), Springer), 298-302
[48] Otten, J., Clausal connection-based theorem proving in intuitionistic first-order logic, (Beckert, B., Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2005), Lect. Notes Comput. Sci., vol. 3702, (2005), Springer), 245-261 · Zbl 1142.03331
[49] Paulson, L.C., 2016. Isabelle’s logics: FOL and ZF.
[50] Rabe, F., The MMT API: A generic MKM system, (Carette, J.; Aspinall, D.; Lange, C.; Sojka, P.; Windsteiger, W., Proc. of the 6th Conference on Intelligent Computer Mathematics (CICM’2013), Lect. Notes Comput. Sci., vol. 7961, (2013), Springer), 339-343 · Zbl 1390.68626
[51] Ramakrishnan, I. V.; Sekar, R. C.; Voronkov, A., Term indexing, (Robinson, J. A.; Voronkov, A., Handbook of Automated Reasoning (in 2 volumes), (2001), Elsevier and MIT Press), 1853-1964 · Zbl 0992.68189
[52] Rotman, J. J., Advanced modern algebra, vol. 114, (2010), American Mathematical Soc. · Zbl 1206.00007
[53] Schulz, S., Simple and efficient clause subsumption with feature vector indexing, (Bonacina, M. P.; Stickel, M. E., Automated Reasoning and Mathematics - Essays in Memory of William W. McCune, Lect. Notes Comput. Sci., vol. 7788, (2013), Springer), 45-67 · Zbl 1383.68082
[54] Slind, K.; Norrish, M., A brief overview of HOL4, (Mohamed, O. A.; Muñoz, C. A.; Tahar, S., TPHOLs, Lect. Notes Comput. Sci., vol. 5170, (2008), Springer), 28-32 · Zbl 1165.68474
[55] So, C. M.; Watt, S. M., On the conversion between content mathml and openmath, (Proc. of the Conference on the Communicating Mathematics in the Digital Era (CMDE’06), (2006)), 169-182
[56] Sutcliffe, G.; Schulz, S.; Claessen, K.; Baumgartner, P., The TPTP typed first-order form with arithmetic, (Bjørner, N.; Voronkov, A., LPAR, Lect. Notes Comput. Sci., vol. 7180, (2012), Springer), 406-419 · Zbl 1352.68217
[57] Trybulec, A., Checker, compiled by freek wiedijk, (2007)
[58] Univalent Foundations Program T, Homotopy type theory: univalent foundations of mathematics, (2013), Institute for Advanced Study · Zbl 1298.03002
[59] Urban, J., Momm - fast interreduction and retrieval in large libraries of formalized mathematics, Int. J. Artif. Intell. Tools, 15, 1, 109-130, (2006)
[60] Urban, J., MPTP 0.2: design, implementation, and initial experiments, J. Autom. Reason., 37, 1-2, 21-43, (2006) · Zbl 1113.68095
[61] Walukiewicz, D., A total AC-compatible reduction ordering on higher-order terms, (Larsen, K. G.; Skyum, S.; Winskel, G., Automata, Languages and Programming, 25th International Colloquium (ICALP’98), Lect. Notes Comput. Sci., vol. 1443, (1998), Springer), 530-542
[62] Wenzel, M.; Paulson, L. C.; Nipkow, T., The isabelle framework, (Mohamed, O. A.; Muñoz, C. A.; Tahar, S., Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Lect. Notes Comput. Sci., vol. 5170, (2008)), 33-38 · Zbl 1165.68478
[63] Whiteside, I.; Aspinall, D.; Dixon, L.; Grov, G., Towards formal proof script refactoring, (Davenport, J. H.; Farmer, W. M.; Urban, J.; Rabe, F., Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Lect. Notes Comput. Sci., vol. 6824, (2011), Springer), 260-275 · Zbl 1335.68240
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.