[SMT-LIB] SMT-LIB collateral licencing

[Grundy, Jim D]

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.
 
Let me just restrict myself to thinking about the logic and theory files
for the moment.  We might like - one day - to distribute the SMT-LIB
logic and theory files with DPT, or some derivatives of those files.  As
it happens you need those files to use DPT, and since the licening of
those files is not known to us we have to direct potential DPT users to
go and get those files for themselves from the SMT-LIB web site.  Not a
big imposition, but it raises the question.
 
I'd like to propose that the copyright for those files be documented in
the standard way with comments in those files. And that further, those
files be licenced under some appropriate licence, with the licence
notice added as comments to those files.
 
So, which licence?  The theory and logic files look more like software
than documentation to me, so lets consider software licenses. There are
lots of good alternatives.  DPT uses the Apache 2 licence, so that would
suite us, but others may have other preferences.  I would express a
strong preference for an license that meets the following criteria:

1. A license that already exists and is fairly common, not something we
make up. 

2. A licence that the Free Software Foundation characterizes as a "Free
Software License".

3. A license that the Open Source Initiative characterizes as an "Open
Source License".

4. A license that the Free Software Foundation does NOT characterize as
a "Copyleft license".

5. A license that the Open Source Initiative does NOT characterize as
either "redundant with a more popular license", "non-reusable",
"superseded", or "retired".

6. A license that the Free Software Foundation characterizes as
compatible with the GPL, at least version 3 there of.

To check out the options surf to:

http://www.fsf.org/licensing/licenses

http://www.opensource.org/licenses/category

Keep your wits about you because there seems to be some degree of
ambiguity about what to call the various BSD/MIT/X style licenses and
these two sites don't necessarily use the same names for them.

Kind regards

Jim Grundy

--
Jim Grundy, Research Scientist. Intel Corporation, Strategic CAD Labs
Mail Stop RA2-451, 2501 NW 229th Ave, Hillsboro, OR 97124-5503, USA
Phone: +1 971 214-1709  Fax: +1 971 214-1771
Key Fingerprint: 5F8B 8EEC 9355 839C D777  4D42 404A 492A AEF6 15E2