大型正式维基百科：问题与解决方案
摘要：面向大型形式化数学维基百科的几个步骤介绍了Coq证明助手和CoRN存储库是通过通用维基系统处理的系统之一，该维基系统在cite{DBLP:conf/aisc/UrbanARG10}中有所描述。基于最近开发的精确跟踪数学依赖性，为维基中的大型形式化库提出了一种智能重验证方案，该方案适用于Mizar/MML和Coq/CoRN。我们建议利用最先进的文件系统功能，允许实时克隆和隔离整个数学库，还可以将维基扩展到真正的多用户协作区域。还讨论了一些相关问题。
作者：Jesse Alama, Kasper Brink, Lionel Mamane and Josef Urban
论文ID：1107.3209
分类：Digital Libraries
分类简称：cs.DL
提交时间：2011-07-27