|
John C. Peterson |
0082d22 |
diff -uNr eqp-09e.orig/LICENSE eqp-09e/LICENSE
|
|
John C. Peterson |
0082d22 |
--- eqp-09e.orig/LICENSE 1969-12-31 16:00:00.000000000 -0800
|
|
John C. Peterson |
0082d22 |
+++ eqp-09e/LICENSE 2017-03-19 18:35:59.791340069 -0700
|
|
John C. Peterson |
0082d22 |
@@ -0,0 +1,138 @@
|
|
John C. Peterson |
0082d22 |
+The EQP source distribution (a compressed tar file) did not include any
|
|
John C. Peterson |
0082d22 |
+information that explicitly stated the terms of the software license.
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+It was not possible to contact the author of EQP, William McCune, as he
|
|
John C. Peterson |
0082d22 |
+sadly passed away in May 2011. The development of EQP was while he was
|
|
John C. Peterson |
0082d22 |
+affiliated with the Argonne National Laboratory, so they were contacted
|
|
John C. Peterson |
0082d22 |
+with the hope of providing clarification of the license terms.
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+The emails received in response to a request for clarification are
|
|
John C. Peterson |
0082d22 |
+included below. Also included is the text of the web pages that hosted
|
|
John C. Peterson |
0082d22 |
+the EQP source distribution that the emails referred us to. The intended
|
|
John C. Peterson |
0082d22 |
+license is presumed to be Public Domain.
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+Date: Thu, 25 Oct 2012 11:18:10 -0500
|
|
John C. Peterson |
0082d22 |
+Message-Id: <9223F4CF-6479-4988-8055-D06DAD2ADF43@mcs.anl.gov>
|
|
John C. Peterson |
0082d22 |
+From: Gail Pieper <pieper@mcs.anl.gov>
|
|
John C. Peterson |
0082d22 |
+To: jcp@eskimo.com
|
|
John C. Peterson |
0082d22 |
+Cc: Larry Wos <wos@mcs.anl.gov>, Gail Pieper <pieper@mcs.anl.gov>
|
|
John C. Peterson |
0082d22 |
+Subject: OTTER and EQP
|
|
John C. Peterson |
0082d22 |
+X-Mailer: Apple Mail (2.1257)
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+Dear John,
|
|
John C. Peterson |
0082d22 |
+Larry asked me to look into the situation about OTTER and EQP.
|
|
John C. Peterson |
0082d22 |
+Here is what our lawyers responded.
|
|
John C. Peterson |
0082d22 |
+Gail Pieper
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+The Otter software (by Bill Otter) was never reported to Legal for an
|
|
John C. Peterson |
0082d22 |
+official meeting and is not in our reported software database.
|
|
John C. Peterson |
0082d22 |
+I looked on the ANL website and found an ANL
|
|
John C. Peterson |
0082d22 |
+website, http://www.mcs.anl.gov/research/projects/AR/otter/#copyright where
|
|
John C. Peterson |
0082d22 |
+Otter is discussed. The webpage has a copyright notice, attached below,
|
|
John C. Peterson |
0082d22 |
+indicating that Otter (at least this Version 3.3) is publically
|
|
John C. Peterson |
0082d22 |
+available. Although it does say on this website that this version is
|
|
John C. Peterson |
0082d22 |
+obsolete and maintained elsewhere.
|
|
John C. Peterson |
0082d22 |
+I hope this helps you.
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+Paul Betten, Ph.D.
|
|
John C. Peterson |
0082d22 |
+Technology Development and Commercialization Division, Bldg 201
|
|
John C. Peterson |
0082d22 |
+Argonne National Laboratory
|
|
John C. Peterson |
0082d22 |
+9700 S. Cass Avenue
|
|
John C. Peterson |
0082d22 |
+Argonne, IL 60564
|
|
John C. Peterson |
0082d22 |
+Tel: (630) 252-4962 fax-5230
|
|
John C. Peterson |
0082d22 |
+e-mail: betten@anl.gov
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+Otter and MACE Legal Page
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+--------------------------------------------------------------------------------
|
|
John C. Peterson |
0082d22 |
+November 21, 2001.
|
|
John C. Peterson |
0082d22 |
+--------------------------------------------------------------------------------
|
|
John C. Peterson |
0082d22 |
+This information refers to the Otter and MACE automated deduction
|
|
John C. Peterson |
0082d22 |
+software, created at Argonne National Laboratory.
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+Copyrights
|
|
John C. Peterson |
0082d22 |
+The University of Chicago has declined to assert its copyrights in this
|
|
John C. Peterson |
0082d22 |
+software. It may be used by the public without restriction and is
|
|
John C. Peterson |
0082d22 |
+available here by download.
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+License
|
|
John C. Peterson |
0082d22 |
+This material resulted from work developed under a U.S. Government
|
|
John C. Peterson |
0082d22 |
+contract and is subject to the following license: the Government is
|
|
John C. Peterson |
0082d22 |
+granted for itself and the public a paid-up, nonexclusive, irrevocable
|
|
John C. Peterson |
0082d22 |
+worldwide license in this material to reproduce, prepare derivative works,
|
|
John C. Peterson |
0082d22 |
+distribute copies to the public, and perform publicly and display
|
|
John C. Peterson |
0082d22 |
+publicly.
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+Disclaimer
|
|
John C. Peterson |
0082d22 |
+NEITHER THE UNITED STATES GOVERNMENT NOR ANY AGENCY THEREOF, NOR ANY OF
|
|
John C. Peterson |
0082d22 |
+THEIR EMPLOYEES OR OFFICERS, MAKES ANY WARRANTY, EXPRESS OR IMPLIED, OR
|
|
John C. Peterson |
0082d22 |
+ASSUMES ANY LEGAL LIABILITY OR RESPONSIBILITY FOR THE ACCURACY,
|
|
John C. Peterson |
0082d22 |
+COMPLETENESS, OR USEFULNESS OF ANY INFORMATION, APPARATUS, PRODUCT, OR
|
|
John C. Peterson |
0082d22 |
+PROCESS DISCLOSED, OR REPRESENTS THAT ITS USE WOULD NOT INFRINGE PRIVATELY
|
|
John C. Peterson |
0082d22 |
+OWNED RIGHTS.
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+Date: Mon, 29 Oct 2012 10:03:34 -0500
|
|
John C. Peterson |
0082d22 |
+Message-Id: <992AF342-1C2D-4E0F-BA6F-4CEF26AE39A5@mcs.anl.gov>
|
|
John C. Peterson |
0082d22 |
+From: Gail Pieper <pieper@mcs.anl.gov>
|
|
John C. Peterson |
0082d22 |
+To: "John C. Peterson" <jcp@eskimo.com>
|
|
John C. Peterson |
0082d22 |
+Subject: Re: OTTER and EQP
|
|
John C. Peterson |
0082d22 |
+X-Mailer: Apple Mail (2.1257)
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+John,
|
|
John C. Peterson |
0082d22 |
+Have you looked at the websites
|
|
John C. Peterson |
0082d22 |
+http://www.mcs.anl.gov/research/projects/AR/eqp/ and
|
|
John C. Peterson |
0082d22 |
+http://www.cs.unm.edu/~mccune/eqp/ ?
|
|
John C. Peterson |
0082d22 |
+If those are not enough, please let me know and I will contact
|
|
John C. Peterson |
0082d22 |
+Paul Betten again.
|
|
John C. Peterson |
0082d22 |
+Gail
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+On Oct 29, 2012, at 2:01 AM, John C. Peterson wrote:
|
|
John C. Peterson |
0082d22 |
+> On Thu, Oct 25, 2012 at 11:18:10AM -0500, Gail Pieper wrote:
|
|
John C. Peterson |
0082d22 |
+>> Dear John,
|
|
John C. Peterson |
0082d22 |
+>> Larry asked me to look into the situation about OTTER and EQP.
|
|
John C. Peterson |
0082d22 |
+>> Here is what our lawyers responded. > Gail Pieper
|
|
John C. Peterson |
0082d22 |
+>
|
|
John C. Peterson |
0082d22 |
+> Hi Gail,
|
|
John C. Peterson |
0082d22 |
+>
|
|
John C. Peterson |
0082d22 |
+> Thanks so much for taking time out to look into these copyright,
|
|
John C. Peterson |
0082d22 |
+> licensing issues for me. I'm volunteering my own time to try and get
|
|
John C. Peterson |
0082d22 |
+> Bill McCune's software packaged so it can be distributed with Fedora
|
|
John C. Peterson |
0082d22 |
+> Linux.
|
|
John C. Peterson |
0082d22 |
+>
|
|
John C. Peterson |
0082d22 |
+> I'm not certain, but I suspect the page you referred me to about
|
|
John C. Peterson |
0082d22 |
+> OTTER may satisfy the Fedora Legal team regarding the issues they
|
|
John C. Peterson |
0082d22 |
+> had. (I haven't heard back from them yet).
|
|
John C. Peterson |
0082d22 |
+>
|
|
John C. Peterson |
0082d22 |
+> I still have a question regarding Bill's EQP software. Should I contact
|
|
John C. Peterson |
0082d22 |
+> Paul Betten (named below) or would it be better to work through you?
|
|
John C. Peterson |
0082d22 |
+>
|
|
John C. Peterson |
0082d22 |
+> Best Regards, John
|
|
John C. Peterson |
0082d22 |
+>
|
|
John C. Peterson |
0082d22 |
+>> Paul Betten, Ph.D.
|
|
John C. Peterson |
0082d22 |
+>> Technology Development and Commercialization Division, Bldg 201
|
|
John C. Peterson |
0082d22 |
+>> Argonne National Laboratory
|
|
John C. Peterson |
0082d22 |
+>> 9700 S. Cass Avenue
|
|
John C. Peterson |
0082d22 |
+>> Argonne, IL 60564
|
|
John C. Peterson |
0082d22 |
+>> Tel: (630) 252-4962 fax-5230
|
|
John C. Peterson |
0082d22 |
+>> e-mail: betten@anl.gov
|
|
John C. Peterson |
0082d22 |
+>
|
|
John C. Peterson |
0082d22 |
+> --
|
|
John C. Peterson |
0082d22 |
+> John C. Peterson, KD6EKQ
|
|
John C. Peterson |
0082d22 |
+> mailto:jcp@eskimo.com
|
|
John C. Peterson |
0082d22 |
+> San Diego, CA U.S.A
|
|
John C. Peterson |
0082d22 |
+>
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+The quoted text below appears on both of the EQP web sites (as of 17 Dec, 2011):
|
|
John C. Peterson |
0082d22 |
+http://www.mcs.anl.gov/research/projects/AR/eqp/
|
|
John C. Peterson |
0082d22 |
+http://www.cs.unm.edu/~mccune/eqp/
|
|
John C. Peterson |
0082d22 |
+
|
|
John C. Peterson |
0082d22 |
+"EQP is not as stable and polished as our main production theorem prover
|
|
John C. Peterson |
0082d22 |
+Otter. But it has obtained several interesting results, and we have
|
|
John C. Peterson |
0082d22 |
+decided to make it available (including the source code) to everyone,
|
|
John C. Peterson |
0082d22 |
+with no restrictions (and of course no warranty). EQP's documentation
|
|
John C. Peterson |
0082d22 |
+is not good, but if you already know Otter, you might not have great
|
|
John C. Peterson |
0082d22 |
+difficulty in learning to use EQP."
|
|
John C. Peterson |
0082d22 |
+
|