[SMT-LIB] SMT-LIB collateral licencing

[Grundy, Jim D]

>> The SMT-LIB effort encompases some intellectual property in the  
>> form of copyrights to the documentation, benchmark files and the
logic and
>> theory files.  I'd like to encourage a discussion of how the
ownership
>> of that property should be recorded and licenced.
>> ...
>
> Some might argue that these theories are closer to math/writing than  
> program code, so perhaps a Creative Commons License?  This is how we  
> license our technical documentation that includes plenty of
mathematics.
>   http://creativecommons.org/ 

Indeed one might.  It looks to me like the SMT-LIB standard document
itself is something we would think of as math/writing and you would want
to chose a license appropriate for that kind of content. 

The benchmark files, on the otherhand, seem more like code.

The theorey and logic files seem to have aspects of both.  Most solvers
ignore them, which makes them look like math/writing, but they are
machine readable in the same format as the benchmark files and are
intended to be usable by a solver (as I now understand it) to check (if
the solver wishes) that it is implementing a logic and theory with at
least the same signature as the one requested - which is codish.

One might have to consult a legal expert (or at very least invest a fair
amount of study and thought) to know which kind of license is more
appropriate.

If one were to use a documentation style license I would be tempted to
consider alternatives the the various creative commons licenses.  You
might consider that to get maximum benefit from the licenced work you
probably want to make both commercial developers and free developers
happy with it.  Commercial developers are going to want something that
is not a copyleft licenses (The "Creative Commons Attribution 2.0"
license is OK by that standard, but not the "Creative Commons
Attribution-Sharealike 2.0" license.)  Free developers would probably
like something that is compatibile with the GPL.  The largest proportion
of open-source projects use the GPL, so should someone oneday want to
develop open source tools around SMT-LIB, there is a reasonable chance
that they might want to use the GPL.  If they wanted to include/modify
SMT-LIB licended artifacts in such a project then they would need to  be
licensed under a GPL compatible license - it doesn't look like the free
software foundation considers any of the Creative Commons License
variants to be compatible with the GPL.  Of course the free software
foundation's own free documentation license isn't compatible with the
GPL either - so apparently this is a pretty though standard to meet.

The fsf's licening page give some analysis of documentation licenses. 

It is also worth noting that the math/writing aspects may treated as
documentation, and documentation is explicityly covered by some free
software licenses (like Apache 2.0), so we may consider such licenses
too - especially perhaps for things like theory and logic files that
seem somewhere in between code and documentation.

Kind regards

Jim Grundy

-----Original Message-----
From: Joseph Kiniry [mailto:kiniry at acm.org] 
Sent: Thursday, October 25, 2007 1:39 AM
To: Grundy, Jim D
Cc: smt-lib at cs.nyu.edu
Subject: Re: SMT-LIB collateral licencing

Hi Jim et al,

On 25 Oct, 2007, at 2:59, Grundy, Jim D wrote:

> Hello SMT-LIBers
>
> The SMT-LIB effort encompases some intellectual property in the  
> form of
> copyrights to the documentation, benchmark files and the logic and
> theory files.  I'd like to encourage a discussion of how the ownership
> of that property should be recorded and licenced.
...snip...

Some might argue that these theories are closer to math/writing than  
program code, so perhaps a Creative Commons License?  This is how we  
license our technical documentation that includes plenty of mathematics.
   http://creativecommons.org/

Joe
---
Joseph Kiniry
School of Computer Science and Informatics
UCD CASL
University College Dublin
http://kind.ucd.ie/
http://srg.cs.ucd.ie/
http://casl.ucd.ie/