A wiki for Mizar: Motivation, considerations, and initial prototype

From AcaWiki
Jump to: navigation, search

Citation: Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers (2010) A wiki for Mizar: Motivation, considerations, and initial prototype. Lecture Notes in Computer Science (RSS)
DOI (original publisher): 10.1007/978-3-642-14128-7_38
Semantic Scholar (metadata): 10.1007/978-3-642-14128-7_38
Sci-Hub (fulltext): 10.1007/978-3-642-14128-7_38
Internet Archive Scholar (search for fulltext): A wiki for Mizar: Motivation, considerations, and initial prototype
Download: http://arxiv.org/abs/1005.4552
Tagged: Computer Science (RSS) wikis (RSS), version control (RSS), DVCS (RSS), formal methods (RSS), proof (RSS), consistency (RSS), proof-checking environments (RSS), Mizar (RSS)

Summary

The authors describe how they used wikis, distributed version control systems, and server-based environments to develop an environment for math collaboration, with the proprietary Mizar system.

Theoretical and Practical Relevance

Mizar's focus on formal correctness leads to ideas that might be applied more widely in wikis. Correctness is seen widely as including consistency (see section 5.1). For instance linking to subsections of articles is problematic because these subsections can be renamed, breaking internal links, and reducing "link coherence". Since Mizar is formal, "change propogation" might be addressed formally.

This was published in an open access journal.