[SMT-LIB] SMT-LIB licenses: your input needed!

[John Matthews]

Hi Cesare,

I asked around at Galois, since we often release open source code. We're fans of the 3-clause BSD license (the FSF calls this the "modified BSD license"), which meets Jim's criteria.

Cheers,
-john

On Mar 7, 2011, at 10:05 PM, Tinelli, Cesare wrote:

> Hi all,
> 
> The issue of properly licensing artifacts created by the SMT-LIB initiative 
> (documents, benchmarks, theory/logic specifications) has come up a few times 
> now. I believe that a policy on that is overdue.
> 
> As you all know, there is a large and bewildering variety of licenses out there
> that could be used or adapted for our needs. Since the initiative is a 
> collective effort, I think it would be appropriate to discuss the issue in this 
> forum and hear a variety of opinions and suggestions.
> 
> Here are a few points, to get the discussion started. I warmly solicit your 
> feedback.
> 
> 
> -----------------
> SMT-LIB standards 
> -----------------
> 
> The SMT-LIB initiative was created with the goal of establishing open standards. 
> There are different views of what an open standard should be, but I think the way 
> SMT-LIB has operated so far reflects most closely the ITU-T definition [1].
> I see no reason to change this course except in the direction of officially 
> adopting some refinement of that definition and consistently following its 
> guidelines. I think Bruce Perens' definition [2] would be a good model for us.
> 
> [1] http://www.itu.int/en/ITU-T/ipr/Pages/open.aspx
> [2] http://perens.com/OpenStandards/Definition.html
> 
> 
> -----------------------------
> Theory and logic declarations
> -----------------------------
> 
> The first point about these is whether they should be released under a source code
> license or not. Since they are mostly (semi-formal) specifications directed intended 
> for people, I would say that a Creative Commons license would be more appropriate.
> 
> Specifically I would go for CC-BY-ND [3], which 
> (1) allows free copy and distribution,
> (2) requires attribution,
> (3) permits no alterations (as alterations would defeat the purpose of the standard).
> 
> A possible tricky aspect is that the catalog of theory and logic declarations 
> evolves with time (addition of new declarations, changes to old ones, etc.). So it 
> is possible for third-party copies to get out of sync with the official version on 
> www.smtlib.org, which is definitely not good. Any suggestions on how to address 
> this problem adequately and with reasonable effort for everybody involved?
> 
> [3] http://creativecommons.org/licenses/by-nd/3.0/
> 
> 
> ----------
> Benchmarks
> ----------
> 
> This is perhaps the trickiest point. First of all, are benchmarks comparable to
> source code? In SMT-LIB 1 they were just formulas, but in SMT-LIB 2 they are 
> command scripts. If they are like source code, what would be an appropriate 
> license? A fairly permissive one, such as the BSD licenses [4], or a copyleft one, 
> such as the GNU licenses [5]? I'm not sure.
> 
> The issue is complicated by the following factors:
> - new benchmarks are provided by several people and organizations, some of whom 
>  might disagree with the license we choose,
> - sometimes benchmarks are translations from other sources, which might have
>  their own license,
> - for a lot of benchmarks already in the library, it is hard to identify/contact
>  the original sources/authors, so we might end up imposing a license unilaterally
>  against the authors' original wishes.
> 
> Any suggestions?
> 
> [4] http://en.wikipedia.org/wiki/BSD_licenses
> [5] http://www.gnu.org/licenses/
> 
> 
> 
> Best,
> 
> 
> Cesare
> 
> 
> 
> 
> 
> 
> 
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2205 bytes
Desc: not available
URL: </pipermail/smt-lib/attachments/20110308/cb0c5917/attachment.bin>