Indexing and Retrieval in a Heterogeneous Formal Library

Dedukti and MMT are both examples of tools that can collect mathematical libraries coming from different systems in a unified but heterogeneous body. Indeed, both tools implement a logical framework where the logics or type systems of the various mathematical assistants can be represented, so that their libraries can be encoded in a single format preserving well-typedness. Still, the images of the various libraries remain disjoint: logical consistency of their union is not granted, the encoding of the various statements differs from logic to logic, and the same mathematical entity remains defined repeatedly and independently. To benefit from the common representation, then, additional tools need to be developed, for example, to translate results encoded in the representation of a logic into the representation of a stronger logic, taking care of aligning the duplicated mathematical entities. In this paper we address the challenges posed by indexing and searching the large, heterogeneous library. For example, users may expect to find results in the library up to the encoding used and up to alignments, so to be able to mix in the search result statements originally coming from different systems and logics. In particular, we describe new indexing and retrieval capabilities that we integrated directly into the LambdaPi proof assistant, that can work on Dedukti files.