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
Large formal wikis: Issues and solutions
2011
alama-large-formal-wikis
We present several steps towards large formal mathematical wikis. The Coq proof assistant together with the CoRN repository are added to the pool of systems handled by the general wiki system described earlier. A smart re-verification scheme for the large formal libraries in the wiki is suggested for Mizar/MML and Coq/CoRN, based on recently developed precise tracking of mathematical dependencies. We propose to use features of state-of-the-art filesystems to allow real-time cloning and sandboxing of the entire libraries, allowing also to extend the wiki to a true multi-user collaborative area. A number of related issues are discussed.
In proceedings
Jesse Alama, Kasper Brink, Lionel Mamane, Josef Urban
James Davenport, William Farmer, Florian Rabe, Josef Urban
Intelligent Computer Mathematics
Lecture Notes in Computer Science
Springer
-
6824
133-148
-
-
-
http://www.springerlink.com/content/qm3203471p33w271
Export formats
Jesse Alama and Kasper Brink and Lionel Mamane and Josef Urban, Large formal wikis: Issues and solutions, 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. 133-148, (http://www.springerlink.com/content/qm3203471p33w271), 2011.
<a href="/people/members/view.php?code=d18f2a73808637adda0742073904f056" class="author">Jesse Alama</a>, Kasper Brink, Lionel Mamane and Josef Urban, <b>Large formal wikis: Issues and solutions</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. 133-148, (<a href="http://www.springerlink.com/content/qm3203471p33w271" target="_blank">url</a>), 2011.
@inproceedings {alama-large-formal-wikis, author = {Jesse Alama and Kasper Brink and Lionel Mamane and Josef Urban}, editor = {James Davenport and William Farmer and Florian Rabe and Josef Urban}, title = {Large formal wikis: Issues and solutions}, booktitle = {Intelligent Computer Mathematics}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, volume = {6824}, pages = {133-148}, url = {http://www.springerlink.com/content/qm3203471p33w271}, abstract = {We present several steps towards large formal mathematical wikis. The Coq proof assistant together with the CoRN repository are added to the pool of systems handled by the general wiki system described earlier. A smart re-verification scheme for the large formal libraries in the wiki is suggested for Mizar/MML and Coq/CoRN, based on recently developed precise tracking of mathematical dependencies. We propose to use features of state-of-the-art filesystems to allow real-time cloning and sandboxing of the entire libraries, allowing also to extend the wiki to a true multi-user collaborative area. A number of related issues are discussed.}, year = {2011}, }
Publication's urls
/publications/view.php?code=bb886224fb1f52826688ee7b4f2710cb
/publications/view.php?code=alama-large-formal-wikis
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