Licensing the Mizar Mathematical Library (MML). The Mizar Mathematical Library (MML) is a large corpus of formalised mathematical knowledge. It has been constructed over the course of many years by a large number of authors and maintainers. Yet the legal status of these efforts of the Mizar community has never been clarified. In 2010, after many years of loose deliberations, the community decided to investigate the issue of licensing the content of the MML, thereby clarifying and crystallizing the status of the texts, the text’s authors, and the library’s long-term maintainers. The community has settled on a copyright and license policy that suits the peculiar features of Mizar and its community. In this paper we discuss the copyright and license solutions. We offer our experience in the hopes that the communities of other libraries of formalised mathematical knowledge might take up the legal and scientific problems that we addressed for Mizar.
Keywords for this software
References in zbMATH (referenced in 47 articles , 2 standard articles )
Showing results 41 to 47 of 47.
- Urban, Josef: MPTP 0.2: Design, implementation, and initial experiments (2006)
- Asperti, Andrea; Zacchiroli, Stefano: Searching mathematics on the web: state of the art and future developments (2005)
- Bancerek, Grzegorz; Urban, Josef: Integrated semantic browsing of the Mizar mathematical library for authoring Mizar articles (2004)
- Cairns, Paul: Informalising formal mathematics: Searching the Mizar library with latent semantics (2004)
- Bancerek, Grzegorz; Rudnicki, Piotr: Information retrieval in MML (2003)
- Urban, Josef: MPTP 0.1 -- system description (2003)
- Rudnicki, Piotr; Trybulec, Andrzej: Mathematical knowledge management in MIZAR (2001)