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.

References in zbMATH (referenced in 48 articles , 2 standard articles )

Showing results 21 to 40 of 48.
Sorted by year (citations)
  1. Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff: ATP and presentation service for Mizar formalizations (2013)
  2. Alama, Jesse; Kühlwein, Daniel; Urban, Josef: Automated and human proofs in general mathematics: an initial comparison (2012)
  3. Alama, Jesse; Mamane, Lionel; Urban, Josef: Dependencies in formal mathematics: applications and extraction for Coq and Mizar (2012)
  4. Kühlwein, Daniel; van Laarhoven, Twan; Tsivtsivadze, Evgeni; Urban, Josef; Heskes, Tom: Overview and evaluation of premise selection techniques for large theory mathematics (2012)
  5. Alama, Jesse: \textttmizar-items: exploring fine-grained dependencies in the \textttMizarMathematical Library (MML) (2011)
  6. Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef: Licensing the Mizar Mathematical Library (MML) (2011)
  7. Davenport, James H. (ed.); Farmer, William M. (ed.); Urban, Josef (ed.); Rabe, Florian (ed.): Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings (2011)
  8. Hoder, Kryštof; Voronkov, Andrei: Sine qua non for large theory reasoning (2011)
  9. Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr: MaLeCoP. Machine learning connection prover (2011)
  10. Caminati, Marco Bright: Basic first-order model theory in Mizar (2010)
  11. Dietrich, Dominik; Schulz, Ewaryst: Crystal: Integrating structured queries into a tactic language (2010)
  12. Urban, Josef; Hoder, Krystof; Voronkov, Andrei: Evaluation of automated theorem proving on the Mizar mathematical library (2010)
  13. Naumowicz, Adam; Korniłowicz, Artur: A brief overview of Mizar (2009)
  14. Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano: User interaction with the Matita proof assistant (2007)
  15. Cairns, Paul; Gow, Jeremy: Integrating searching and authoring in Mizar (2007)
  16. Grabowski, Adam; Schwarzweller, Christoph: Revisions as an essential tool to maintain mathematical repositories (2007)
  17. Urban, Josef; Bancerek, Grzegorz: Presenting and explaining Mizar (2007)
  18. Asperti, Andrea; Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano: A content based mathematical search engine: Whelp (2006)
  19. Bancerek, Grzegorz: Information retrieval and rendering with MML Query (2006)
  20. Urban, Josef: MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics (2006)