Computer Science – Digital Libraries
Scientific paper
2011-07-16
Intelligent Computer Mathematics 2011, LNCS 6824, pp. 149-165
Computer Science
Digital Libraries
To appear in The Conference of Intelligent Computer Mathematics: CICM 2011
Scientific paper
10.1007/978-3-642-22673-1_11
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 in \cite{DBLP:conf/aisc/UrbanARG10}. 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.
Alama Jesse
Brink Kasper
Mamane Lionel
Urban Josef
No associations
LandOfFree
Large Formal Wikis: Issues and Solutions does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Large Formal Wikis: Issues and Solutions, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Large Formal Wikis: Issues and Solutions will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-550333