[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Two license questions



    Dear list,

I intend to package two theorem provers, otter and spass, and a
model builder, mace. Before I post the official ITP, I want to
make sure the legal stuff.

Otter and mace are distributed under a common license, which
seems to be suitable for them to go into main. I attach this
license below.

Spass seems to be a little more difficult. (See license
attached.) It restricts re-distribution to "non-commercial" and
"non-safety-critical" purposes. This probably means that it has
to go into non-free, right? What troubles me is the following
paragraph:

    If you refer to the performance of SPASS in any
    result/experiment made public in any way, you must cite the
    version of SPASS. Moreover, any data needed to reproduce
    such a result/experiment must be publicly available.

What implications does that have for Debian?

    Any comments are appreciated,
    Marco

-- 
Marco Kuhlmann                                      mk@debian.org
Otter and MACE Legal Information

November 21, 2001.

This information refers to the Otter and MACE automated deduction
software, created at Argonne National Laboratory.

Copyrights

The University of Chicago has declined to assert its
copyrights in this software.  It may be used by the public without
restriction and is available by download at www.mcs.anl.gov/AR/otter/.

License

This material resulted from work developed under a U.S. Government contract 
and is subject to the following license: the Government is granted for 
itself and the public a paid-up, nonexclusive, irrevocable worldwide 
license in this material to reproduce, prepare derivative works, distribute 
copies to the public, and perform publicly and display publicly.

Disclaimer

NEITHER THE UNITED STATES GOVERNMENT NOR ANY AGENCY THEREOF, NOR ANY OF 
THEIR EMPLOYEES OR OFFICERS, MAKES ANY  WARRANTY, EXPRESS OR IMPLIED, OR 
ASSUMES ANY LEGAL LIABILITY OR RESPONSIBILITY FOR THE ACCURACY, 
COMPLETENESS, OR USEFULNESS OF ANY INFORMATION, APPARATUS, PRODUCT, OR 
PROCESS DISCLOSED, OR REPRESENTS THAT ITS USE WOULD NOT INFRINGE PRIVATELY 
OWNED RIGHTS.

SPASS is an experimental implementation of
a theorem prover for full first-order logic
with equality. The tools dfg2otter.pl and dfg2tptp
translate files in the SPASS DFG syntax in
otter or tptp syntax, respectively. The scripts/binaries
pcs and pgen can be employd for proof checking.


We take no responsibility for any effect caused by this software. 
It is provided "AS IS" without express or implied warranty.  
In particular, it must be understood that this software is an 
experimental version, and is not suitable for use in any 
safety-critical application, and the authors deny a license for   
such use.                                                              
                                                                          
You may use, copy, modify and distribute this software for any         
non-commercial and non-safety-critical purpose.  Use of this software   
in a commercial product is not included under this license.  You must  
maintain this copyright statement in all copies of this software that  
you modify or distribute.  

If you refer to the performance of SPASS in any result/experiment made 
public in any way, you must cite the version of SPASS. Moreover, any
data needed to reproduce such a result/experiment must be publicly available.

Although we tested SPASS and the tools and spent effort in making
them reliable, it is not unlikely that
they still contain bugs. Any comments or bug reports 
are highly appreciated. Please send comments and
bug reports to 

	spass@mpi-sb.mpg.de 

with subject COMMENT or BUG, respectively. Don't forget to provide 
all data necessary  to reproduce the discovered problems or to 
understand your  comments. This typically includes your platform, 
the SPASS (tool) version, input file or compiler settings if you started 
from sources.

Consult the SPASS homepage
	
		http://spass.mpi-sb.mpg.de/

for recent developments and information.


Have SPASS
 Christoph Weidenbach





Attachment: pgp4UeowFneZg.pgp
Description: PGP signature


Reply to: