[mizar] Fwd: License for MML

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

---------- Forwarded message ----------
From: Dr. Stephan Schulz <schulz@informatik.tu-muenchen.de>
Date: Tue, Feb 23, 2010 at 9:39 AM
Subject: Re: License for MML
To: Josef Urban <josef.urban@gmail.com>



Hi Josef!

Not it gets tricky...

On 23 Feb 2010, at 01:16, Josef Urban wrote:
>>
>
> It would seem good to dual-license MML under CC-BY-SA and (L)GPL .
>
> However, the last link above talks about the dangers of dual
> licensing. Is it true that if we dual license as above,
> copying/modifying proofs from Wikipedia/PlanetMath will not be
> possible, because WP/PlanetMath are not released under (L)GPL?


In principle, if you want to use certain protected material, you need
to abide by its license conditions (or claim fair use). In particular,
no, you cannot take material that is only released under one license
and re-release it under a different license or combination of licenses.

An interesting question is in how far proofs are protected material.
In general, mathematical results are not protected by copyright.
However, the _expression_ of these results is. Computer programs
are protected - considering the "proofs as programs" paradigm, this
may or may not translate to proofs. On the other hand, is there really
creative input that worthy of protection if someone runs
"eprover -xAuto -tAuto --tptp3-in goldbach.p" ?

I don't think this is something that has much settled precedent. It
might be a good idea to contact the Software Freedom Law Center
(http://www.softwarefreedom.org/) to see if they an provide an opinion
and some help.

Bye,

    Stephan

--
-------------------------- It can be done! ---------------------------------
  Please email me as schulz@informatik.tu-muenchen.de (Stephan Schulz)
----------------------------------------------------------------------------