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

[Grundy, Jim D]

With regard to the benchmarks... it will be difficult to get folks to sign up to a standard license, but I think it's worth doing and the longer you leave it the harder it gets. The Boost folks left it quite a while and it took a lot of work for them to go back and get everything consistently licensed later - which they eventually found they needed to do.

For source code licenses I favor a license that is:

- not copy-left
- is considered by the FSF to be a "GPL-Compatible Free Software License" as listed here: http://www.gnu.org/licenses/license-list.html
- is considered by the Open Source Initiative to be an open source licenses that is on their list of licenses that are "popular and widely used or with strong communities" as listed here: http://www.opensource.org/licenses/category

Pick any license that meets those criteria and, IMHO, you can't go too far wrong.

All the best

Jim

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Tinelli, Cesare
Sent: Monday, 07 March, 2011 22:05
To: smt-lib
Subject: [SMT-LIB] SMT-LIB licenses: your input needed!

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