Abstract
Many proof assistant libraries contain formalizations of the same mathematical concepts. The concepts are often introduced (defined) in different ways, but the properties that they have, and are in turn formalized, are the same. For the basic concepts, like natural numbers, matching them between libraries is often straightforward, because of mathematical naming conventions. However, for more advanced concepts, finding similar formalizations in different libraries is a non-trivial task even for an expert.
In this paper we investigate automatic discovery of similar concepts across libraries of proof assistants. We propose an approach for normalizing properties of concepts in formal libraries and a number of similarity measures. We evaluate the approach on HOL based proof assistants HOL4, HOL Light and Isabelle/HOL, discovering 398 pairs of isomorphic constants and types.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bortin, M., Johnsen, E.B., Lüth, C.: Structured formal development in Isabelle. Nordic Journal of Computing 13, 1–20 (2006)
Carlisle, D., Davenport, J., Dewar, M., Hur, N., Naylor, W.: Conversion between MathML and OpenMath. Technical Report 24.969. The OpenMath Society (2001)
Furbach, U., Shankar, N. (eds.): IJCAR 2006. LNCS (LNAI), vol. 4130. Springer, Heidelberg (2006)
Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100–115. Springer, Heidelberg (2013)
Harrison, J.: Towards self-verification of HOL Light. In: Furbach, Shankar (eds.) [3], pp. 177–191
Harrison, J.: HOL Light: An overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009)
Harrison, J.: The HOL Light theory of euclidean space. J. Autom. Reasoning 50(2), 173–190 (2013)
Heras, J., Komendantskaya, E.: Proof pattern search in Coq/SSReflect. arXiv preprint, CoRR, abs/1402.0081 (2014)
Hurd, J.: The OpenTheory standard theory library. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 177–191. Springer, Heidelberg (2011)
Kaliszyk, C., Krauss, A.: Scalable LCF-style proof translation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 51–66. Springer, Heidelberg (2013)
Kaliszyk, C., Urban, J.: Lemma mining over HOL Light. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol. 8312, pp. 503–517. Springer, Heidelberg (2013)
Kaliszyk, C., Urban, J.: HOL(y)Hammer: Online ATP service for HOL Light. arXiv preprint abs/1309.4962, accepted for publication in Mathematics in Computer Science (2014)
Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. arXiv preprint abs/1211.7012, accepted for publication in Journal of Automated Reasoning (2014)
Keller, C., Werner, B.: Importing HOL Light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 307–322. Springer, Heidelberg (2010)
Mohamed, O.A., Muñoz, C., Tahar, S. (eds.): TPHOLs 2008. LNCS, vol. 5170. Springer, Heidelberg (2008)
Obua, S., Skalberg, S.: Importing HOL into Isabelle/HOL. In: Furbach, Shankar (eds.) [3], pp. 298–302
Rabe, F.: The MMT API: A generic MKM system. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 339–343. Springer, Heidelberg (2013)
Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, et al. (eds.) [15], pp. 28–32
So, C.M., Watt, S.M.: On the conversion between content MathML and OpenMath. In: Proc. of the Conference on the Communicating Mathematics in the Digital Era (CMDE 2006), pp. 169–182 (2006)
Urban, J.: MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. on Artificial Intelligence Tools 15(1), 109–130 (2006)
Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, et al. (eds.) [15], pp. 33–38
Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol. 3600. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Gauthier, T., Kaliszyk, C. (2014). Matching Concepts across HOL Libraries. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds) Intelligent Computer Mathematics. CICM 2014. Lecture Notes in Computer Science(), vol 8543. Springer, Cham. https://doi.org/10.1007/978-3-319-08434-3_20
Download citation
DOI: https://doi.org/10.1007/978-3-319-08434-3_20
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08433-6
Online ISBN: 978-3-319-08434-3
eBook Packages: Computer ScienceComputer Science (R0)