MML swMATH ID: 6970 Software Authors: http://mizar.org/people/ Description: 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. Homepage: http://mizar.org/library/ Related Software: Mizar; MPTP 0.2; MoMM; E Theorem Prover; MPTP; Coq; VAMPIRE; MizarMode; MaLARea; HOL Light; SPASS; TPTP; Whelp; Sledgehammer; z3; Isabelle; MaLeCoP; Isar; Isabelle/HOL; OTTER Cited in: 47 Publications Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year Tools for MML environment analysis. Zbl 1417.68213Naumowicz, Adam 2015 Information retrieval in MML. Zbl 1022.68610Bancerek, Grzegorz; Rudnicki, Piotr 2003 all top 5 Cited by 48 Authors 19 Urban, Josef 6 Alama, Jesse 5 Bancerek, Grzegorz 4 Kaliszyk, Cezary 4 Korniłowicz, Artur 4 Naumowicz, Adam 4 Rudnicki, Piotr 4 Sacerdoti Coen, Claudio 3 Asperti, Andrea 3 Grabowski, Adam 3 Guidi, Ferruccio 3 Kühlwein, Daniel 3 Pąk, Karol 3 Voronkov, Andrei 3 Zacchiroli, Stefano 2 Cairns, Paul 2 Caminati, Marco Bright 2 Heskes, Tom M. 2 Hoder, Kryštof 2 Mamane, Lionel Elie 2 Tassi, Enrico 2 Tsivtsivadze, Evgeni 2 Vyskočil, Jiří 1 Blanchette, Jasmin Christian 1 Byliński, Czesław 1 Davenport, James Harold 1 Dietrich, Dominik 1 Färber, Michael 1 Farmer, William M. 1 Gow, Jeremy 1 Haslbeck, Maximilian P. L. 1 Koch, Sebastian 1 Kohlhase, Michael 1 Kotel’nikov, Evgeny A. 1 Kovács, Laura Ildikó 1 Matichuk, Daniel 1 Matuszewski, Roman 1 Nakasho, Kazuhisa 1 Nipkow, Tobias 1 Rabe, Florian 1 Rosolini, Giuseppe 1 Schulz, Ewaryst 1 Schulz, Stephan 1 Schwarzweller, Christoph 1 Shidama, Yasunari 1 Sutcliffe, Geoff 1 Trybulec, Andrzej 1 van Laarhoven, Twan all top 5 Cited in 7 Serials 12 Journal of Automated Reasoning 2 Formalized Mathematics 1 Computer Languages, Systems & Structures 1 Journal of Applied Logic 1 Lecture Notes in Computer Science 1 Mathematics in Computer Science 1 Journal of Formalized Reasoning all top 5 Cited in 7 Fields 44 Computer science (68-XX) 8 Mathematical logic and foundations (03-XX) 2 General and overarching topics; collections (00-XX) 1 Combinatorics (05-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Number theory (11-XX) 1 Real functions (26-XX) Citations by Year