[mizar] License for MML

[Josef Urban <josef.urban@gmail.com>]

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