Result: 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. Logical Frameworks, Interoperability and SearchingInteroperability between different mathematical systems remains a challenging goal despite the amount of research invested into it in the past years. One old approach to it, that has been recently revived by at least the Deducteam 3 and the MMT teams 4 , consists in adopting a single logical framework, express every logic/type theory into it and export the libraries of mathematical results, developed in the various systems, into the common logical framework, obtaining a huge, heterogeneous mathematical library.The encoding of logics and type theories is designed so that well-typed terms that are in the image of the encodings guarantee that the original expression 3