Information Retrieval in MML

  • Grzegorz Bancerek
  • Piotr Rudnicki
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2594)


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.


Information Retrieval Query Language Visible Argument Mizar Mathematical Library Resource Code 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.Google Scholar
  2. 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
  3. 5.
  4. 6.
    P. Rudnicki, Ch. Schwarzweller and A. Trybulec. Commutative Algebra in the Mizar System. Journal of Symbolic Computation, 32:143–169, 2001.MathSciNetCrossRefGoogle Scholar
  5. 7.
    Piotr Rudnicki and Andrzej Trybulec. On equivalents of well-foundedness. Journal of Automated Reasoning, 23(3–4):197–234, 1999.MathSciNetCrossRefGoogle Scholar
  6. 8.
    Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.Google Scholar
  7. 9.
    Wojciech A. Trybulec. Partially ordered sets. Formalized Mathematics, 1(2):313–319, 1990.Google Scholar
  8. 10.
    Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990.Google Scholar
  9. 11.
    Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.Google Scholar
  10. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Grzegorz Bancerek
    • 1
    • 2
  • Piotr Rudnicki
    • 3
  1. 1.Institute of Computer ScienceBiałystok Technical UniversityPoland
  2. 2.Dept. of Information EngineeringShinshu UniversityNaganoJapan
  3. 3.Dept. of Computing ScienceUniversity of AlbertaEdmontonCanada

Personalised recommendations