Matching Concepts across HOL Libraries

Thibault Gauthier and Cezary Kaliszyk

Proceedings of the 7th Conference on Intelligent Computer Mathematics (CICM 2014), Lecture Notes in Computer Science 8543, pp. 267 – 281, 2014. .


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.


  PDF |    doi:10.1007/978-3-319-08434-3_20  |  © Springer International Publishing Switzerland


author = "Thibault Gauthier and Cezary Kaliszyk",
title = "Matching Concepts across {HOL} Libraries",
booktitle = "Proceedings of the 7th Conference on Intelligent Computer Mathematics",
editor = "Stephen Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban",
series = "Lecture Notes in Computer Science",
volume = 8543,
pages = "267--281",
publisher = "Springer-Verlag",
year = 2014,
doi = "10.1007/978-3-319-08434-3_20"
Nach oben scrollen