MML
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 42 articles , 2 standard articles )
Showing results 1 to 20 of 42.
Sorted by year (- Koch, Sebastian: About quotient orders and ordering sequences (2017)
- Guidi, Ferruccio; Sacerdoti Coen, Claudio: A survey on retrieval of mathematical knowledge (2016)
- Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol; Urban, Josef: Mizar: state-of-the-art and beyond (2015)
- Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias: Mining the Archive of Formal Proofs (2015)
- Guidi, Ferruccio; Sacerdoti Coen, Claudio: A survey on retrieval of mathematical knowledge (2015)
- Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
- Kaliszyk, Cezary; Urban, Josef: MizAR 40 for Mizar 40 (2015)
- Korniłowicz, Artur: Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization (2015)
- Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A first class Boolean sort in first-order theorem proving and TPTP (2015)
- Nakasho, Kazuhisa; Shidama, Yasunari: Documentation generator focusing on symbols for the HTML-ized Mizar Library (2015)
- Naumowicz, Adam: Tools for MML environment analysis (2015)
- Pąk, Karol: Readable formalization of Euler’s partition theorem in mizar (2015)
- Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef: Premise selection for mathematics by corpus analysis and kernel methods (2014)
- Grabowski, Adam: Cauchy mean theorem (2014)
- Alama, Jesse: Eliciting implicit assumptions of Mizar proofs by property omission (2013)
- Caminati, Marco Bright; Rosolini, Giuseppe: Custom automations in Mizar (2013)
- Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff: ATP and presentation service for Mizar formalizations (2013)
- Alama, Jesse; Kühlwein, Daniel; Urban, Josef: Automated and human proofs in general mathematics: an initial comparison (2012)
- Alama, Jesse; Mamane, Lionel; Urban, Josef: Dependencies in formal mathematics: applications and extraction for Coq and Mizar (2012)
- Kühlwein, Daniel; van Laarhoven, Twan; Tsivtsivadze, Evgeni; Urban, Josef; Heskes, Tom: Overview and evaluation of premise selection techniques for large theory mathematics (2012)