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

[Tinelli, Cesare]

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