Back to first pageBack to first page Centre for Artificial Intelligence of UNL
Browse our site
You are here:

Publication details

Go back
Publication details
Main information
mizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library
2011
alama-mizar-items
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.
In proceedings
Jesse Alama
James Davenport, William Farmer, Florian Rabe, Josef Urban
Intelligent Computer Mathematics
Lecture Notes in Computer Science
Springer
-
6824
276-277
-
-
-
http://www.springerlink.com/content/e50380424482807p/
Export formats
Jesse Alama, mizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library, in: James Davenport and William Farmer and Florian Rabe and Josef Urban (eds), Intelligent Computer Mathematics, Lecture Notes in Computer Science, Springer, Vol. 6824, Pag. 276-277, (http://www.springerlink.com/content/e50380424482807p/), 2011.
<a href="/people/members/view.php?code=d18f2a73808637adda0742073904f056" class="author">Jesse Alama</a>, <b>mizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library</b>, in: James Davenport, William Farmer, Florian Rabe and Josef Urban (eds), <u>Intelligent Computer Mathematics</u>, Lecture Notes in Computer Science, <a href="http://www.springer.com" title="Link to external entity..." target="_blank" class="publisher">Springer</a>, Vol. 6824, Pag. 276-277, (<a href="http://www.springerlink.com/content/e50380424482807p/" target="_blank">url</a>), 2011.
@inproceedings {alama-mizar-items, author = {Jesse Alama}, editor = {James Davenport and William Farmer and Florian Rabe and Josef Urban}, title = {mizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library}, booktitle = {Intelligent Computer Mathematics}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, volume = {6824}, pages = {276-277}, url = {http://www.springerlink.com/content/e50380424482807p/}, abstract = {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.}, year = {2011}, }
Publication's urls
/publications/view.php?code=f0aae8010f878dab79a51d827b64dc74
/publications/view.php?code=alama-mizar-items
Go back
Centre for Artificial Intelligence of UNL
Departamento de Informática, FCT/UNL
Quinta da Torre 2829-516 CAPARICA - Portugal
Tel. (+351) 21 294 8536 FAX (+351) 21 294 8541

Fundacao_FCT