[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] License for MML

Dear Josef, dear all,

let a longtime lurker on the Mizar list give his 2cents.

  1. It is very important to have an explicit and  well-documented licensing scheme for a collection like Mizar. Thus Andrzej's an dJosef's initiative is very laudable.
  2. Josef mentions various licensing schemes: BSD, GPL, GFDL, CC-BY-SA; my understanding of this is that BSD and GPL work well for code, but not really for documents and data collections. GFDL has been developed for program documentation, but has fallen out of favor (e.g. Wikipedia changed away from it), since it has some provisos (for instance that the cover text has to be preserved) that are not suitable for digital content. That leaves the Creative Commons licenses, of which CC-BY-SA is only one. It shares the viral flavor of the GPL and the GFDL, which I agree with Josef is good for projects/libraries like MIZAR. But even if you go for CopyLeft, then you may still decide whether you restrict licensing to non-commercial contexts. This may or may not be what you have in mind for MIZAR. 
  3. another advantage is that CC licensing is available in many juridical systems, and has been tested in courts (but GPL has been tested better). 
It seems to me that probably CC-BY-SA or CC-BY-SA-noncommercial are the best choices for MIZAR. And indeed this allows the author to keep his/her copyright, which is also a good thing. Conceivably the Association of Mizar users might cease to exist before the interest in the MIZAR library runs out (this is hardly conceivable).

Michael

On 21.02.10 17:43, Josef Urban wrote: 
Dear all,

Andrzej Trybulec has today suggested that we start searching for a
good licensing and submission rules for the Mizar formalizations and
MML, and reach some decision in a historically short time.

Why is the current situation (probably) not good:

- It is not clear under what rules MML can be used (for instance I
translated it to TPTP, part of it was included into the TPTP library,
and consequently used for testing/benchmarking ATPs - was this legal
or not?).

- It seems that the copyright to MML belongs to the Association of
Mizar Users, and that submissions to MML have to "transfer the
copyright". I don't know how well-defined is "transfer of copyright"
in various jurisdictions, and if we need this. It seems more common
that the copyright stays with the authors (or the people that modify
articles), and they just releases their work under a suitable
open-source license (like in Wikipedia and PlanetMath).

My current state of mind (after some discussions with Jesse Alama):

- is to have the Wikipedia/PlanetMath licensing and submission policy.
I am not a lawyer, however it seems to me that the original author can
license his work under multiple licenses (GPL, BSD, etc), and
Wikipedia/PlanetMath just forces him to license also by their Creative
Commons license (CC-BY-SA - link below), in order to make his work
available to others for modification. Having in MML works that are not
freely available for modification sounds like a waste of resources to
me.

- I don't completely understand the differences and their implications
between GPL, GFDL, BSD, Wikipedia/Planetmath (CC-BY-SA). My limited
understanding is that BSD does not force the people who re-use to
provide their work under the same terms, while the other licenses
(GPL, GFDL, CC-BY-SA) do. The idea is that this helps the growth of
the public project (contributing back). There is probably a lot
written on this topic, but the fact that this is successfully used by
Linux, Wikipedia, and PlanetMath is good enough for me.

Some resources:

- Here is the Linux Developer's Certificate of Origin:
http://elinux.org/Developer_Certificate_Of_Origin
- Isabelle submissions seems to be either BSD or GPL licensed
- Here is the Isabelle AFP submission guide and template :
http://afp.sourceforge.net/submitting.shtml
http://afp.sourceforge.net/submit-template
- Here is the summary of the current Wikipedia license:
http://en.wikipedia.org/wiki/Wikipedia:Text_of_Creative_Commons_Attribution-ShareAlike_3.0_Unported_License
- Here is the licensing of Planetmath: http://planetmath.org/?op=license

This is a request for comments, but please keep this discussion
reasonably constructive. It is not a flamebait of any kind, but an
announcement that we would like to solve this issue reasonably well
and in reasonably short time (weeks or days possibly).

Best,
Josef Urban
  

-- 
----------------------------------------------------------------------
 Prof. Dr. Michael Kohlhase,        Office: Research 1, Room 62 
 Professor of Computer Science  Campus Ring 1, 
 Jacobs University Bremen           D-28759 Bremen, Germany
 tel/fax: +49 421 200-3140/-493140  skype: m.kohlhase   
 m.kohlhase@jacobs-university.de http://kwarc.info/kohlhase 
----------------------------------------------------------------------