Friday 22 January 2016, 10:30, LSV: Matching concepts across formalized libraries Thibault Gauthier (University of Innsbruck).

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 talk, 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 generality and efficiency of the approach in experiments with HOL based proof assistants, Coq, Matita and Mizar.