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

From AcaWiki
Revision as of 05:29, 17 February 2011 by Benjamin Mako Hill (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
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: 10.1007/978-3-642-14128-7_38

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)


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.