Abstract
Formal mathematics has so far not taken full advantage of ideas from collaborative tools such as wikis and distributed version control systems (DVCS). We argue that the field could profit from such tools, serving both newcomers and experts alike. We describe a preliminary system for such collaborative development based on the Git DVCS. We focus, initially, on the Mizar system and its library of formalized mathematics.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
The Archive of Formal Proofs, http://afp.sourceforge.net/
Wikiwikiweb, http://c2.com/cgi/wiki?WikiWikiWeb
Corbineau, P., Kaliszyk, C.: Cooperative repositories for formal proofs. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 221–234. Springer, Heidelberg (2007)
Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the Constructive coq Repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 88–103. Springer, Heidelberg (2004)
D’Silva, V., Kroening, D., Weissenbacher, G.: A Survey of Automated Techniques for Formal Software Verification. IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems 27(7), 1165–1178 (2008)
Git - fast version control system, http://git-scm.com/
Gonthier, G.: Formal proof—the four-color theorem. Notices of the American Mathematical Society 55(11), 1382–1393 (2008)
Hales, T.: A proof of the Kepler conjecture. Annals of Mathematics 162(3), 1065–1185 (2005)
Hales, T.: Formal proof. Notices of the American Mathematical Society 55(11), 1370–1381 (2008)
Harrison, J.: Formal Proof – Theory and Practice. Notices of the American Mathematical Society 55, 1395–1406 (2008)
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Anderson, T. (ed.) Proceedings of the 22nd ACM Symposium on Operating Systems Principles, pp. 207–220. ACM Press, New York (2009)
Mathoverflow, http://mathoverflow.net/
Wolfram MathWorld: The Web’s Most Extensive Mathematics Resource, http://mathworld.wolfram.com/
Matuszewski, R., Rudnicki, P.: MIZAR: the first 30 years. Mechanized Mathematics and its Applications 4(1), 3–24 (2005)
The Mizar Mathematical Library, http://mizar.org/library/
Naumowicz, A., Kornilowicz, A.: A Brief Overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 67–72. Springer, Heidelberg (2009)
Planetmath, http://planetmath.org/
The polymath blog, http://polymathprojects.org/
Proofwiki, http://www.proofwiki.org/wiki/Main_Page
The QED Manifesto. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 238–251. Springer, Heidelberg (1994)
The QPQ Deductive Software Repository, http://www.qpq.org
Rudnicki, P., Trybulec, A.: On the integrity of a repository of formalized mathematics. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 162–174. Springer, Heidelberg (2003)
Trigdell, A.: Efficient Algorithms for Sorting and Synchronization. Ph.D. thesis, Australian National University (1999)
Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning 37(1-2), 21–43 (2006)
vdash: What is vdash?, http://www.vdash.org/intro/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Urban, J., Alama, J., Rudnicki, P., Geuvers, H. (2010). A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. In: Autexier, S., et al. Intelligent Computer Mathematics. CICM 2010. Lecture Notes in Computer Science(), vol 6167. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14128-7_38
Download citation
DOI: https://doi.org/10.1007/978-3-642-14128-7_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14127-0
Online ISBN: 978-3-642-14128-7
eBook Packages: Computer ScienceComputer Science (R0)