Information Retrieval in MML
- 308 Downloads
Mizar, a proof-checking system, is used to build the Mizar Mathematical Library (MML). This is a long term project aiming at building a comprehensive library of mathematical knowledge. We describe issues concerning information retrieval, i.e., searching, browsing and presentation of MML contents. A web-based tool providing such functionalities is being implemented by G. Bancerek. We hope that our observations are helpful when solving similar problems for other repositories of formalized mathematics.
KeywordsInformation Retrieval Query Language Visible Argument Mizar Mathematical Library Resource Code
Unable to display preview. Download preview PDF.
- 1.Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.Google Scholar
- 2.David Delahaye. Information Retrieval in a Coq Proof Library using Type Isomorphisms. In T. Coquand et al., editors, TYPES, volume 1956 of LNCS, pages 131–147. Springer, 2000.Google Scholar
- 5.Mizar Manuals. http://mizar.org/project/bibliography.html.
- 8.Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.Google Scholar
- 9.Wojciech A. Trybulec. Partially ordered sets. Formalized Mathematics, 1(2):313–319, 1990.Google Scholar
- 10.Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990.Google Scholar
- 11.Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.Google Scholar
- 12.Mariusz Żynel and Czesław Byliński. Properties of relational structures, posets, lattices and maps. Formalized Mathematics, 6(1):123–130, 1997.Google Scholar