The MML is one of the largest collection of formalized mathematical knowledge that has been developed with various interactive proof assistants. It comprises more than 1100 "articles" summing to nearly 2.5 million lines of text, each consisting of a unified collection of mathematical definitions and proofs. Semantically, it contains more than 50000 theorems and more than 10000 definitions expressed using more than 7000 symbols. It thus offers a fascinating corpus on which one could carry out a number of experiments. This note discusses a system for computing fine-grained dependencies among the contents of the MML. For an overview of Mizar, see [3]; for a discussion of some successful initial experiments carried out with the help of mizar-items, see [1,2]. © 2011 Springer-Verlag.
CITATION STYLE
Alama, J. (2011). mizar-items: Exploring fine-grained dependencies in the Mizar mathematical library. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6824 LNAI, pp. 276–277). https://doi.org/10.1007/978-3-642-22673-1_19
Mendeley helps you to discover research relevant for your work.