[Fedora-legal-list] Legal opinion on license for EQP

[John C. Peterson]

On Wed, Jan 04, 2012 at 10:42:35AM -0500, Tom Callaway wrote:
> On 01/03/2012 04:35 PM, John C. Peterson wrote:
> > "... and we have decided
> > to make it available (including the source code) to everyone, with no
> > restrictions (and of course no warranty)."
> 
> IMHO, this is not sufficient to constitute a Free Software License,
> notably, because there is no clear permission to modify in the above
> statement. (Although it says "with no restrictions", the way that
> copyright law works in the US is that the copyright holder must
> explicitly grant rights which are not offered by default, ...
> 
> I think contacting ANL would be the next step if you wished to pursue
> resolving this licensing issue.

Thanks for the opinions. Bill (the author) had an appointment as a
research professor at Univ of New Mexico for the last few years, which
is where the project is currently hosted. Karsten is correct that the
bulk of his work on EQP was while he was at Argonne National Labs, so
they are probably the rightful owner of the copyright. Bill worked for
Larry Wos while at ANL, and he is still there, so getting in contact with
the relevant people is not a big problem. I am certainly willing to do
that yeoman's work.

On Tue, Jan 03, 2012 at 03:35:12PM -0800, Karsten 'quaid' Wade wrote:
> Another problem that you don't bring up is, with the upstream project
> permanently in limbo, where do you take bugs for fixing, etc.? Are you
> thinking of starting a new project page somewhere for that?

That is something that I was not planning on doing. I'm still new to
the packaging process - is the absence of an upstream a show stopper?

EQP is most certainly still a very useful program, but my reason for
wanting to package it is more historical in nature. Here is the part
of the package description from the spec file that explains its role in
theorem proving history:

"In the early 1930's, it was postulated that every Robbin's Algebra, named
after Herbert Ellis Robbins, must also be a Boolean Algebra.  Many (human)
mathematicians attempted to find a formal proof, or a counter-example of
this conjecture. The EQP automated theorem prover (and its author William
McCune) made history by providing the first known proof in 1996."

The rest of the package review is here;

https://bugzilla.redhat.com/show_bug.cgi?id=769958

John

-- 
John C. Peterson, KD6EKQ
mailto:jcp at eskimo.com
San Diego, CA U.S.A