Debian Bug report logs - #681043
O: otter -- resolution-style theorem prover

Package: wnpp; Maintainer for wnpp is wnpp@debian.org;

Reported by: Ricardo Mones <mones@debian.org>

Date: Tue, 10 Jul 2012 08:51:02 UTC

Severity: normal

Reply or subscribe to this bug.

Toggle useless messages

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to debian-bugs-dist@lists.debian.org, pcc03@doc.ic.ac.uk, wnpp@debian.org:
Bug#681043; Package wnpp. (Tue, 10 Jul 2012 08:51:06 GMT) Full text and rfc822 format available.

Acknowledgement sent to Ricardo Mones <mones@debian.org>:
New Bug report received and forwarded. Copy sent to pcc03@doc.ic.ac.uk, wnpp@debian.org. (Tue, 10 Jul 2012 08:51:45 GMT) Full text and rfc822 format available.

Message #5 received at submit@bugs.debian.org (full text, mbox):

From: Ricardo Mones <mones@debian.org>
To: submit@bugs.debian.org
Subject: O: otter -- resolution-style theorem prover
Date: Tue, 10 Jul 2012 10:47:21 +0200
[Message part 1 (text/plain, inline)]
Package: wnpp
Severity: normal

The current maintainer of otter, Peter Collingbourne <pcc03@doc.ic.ac.uk>,
is not interested in it anymore.  Therefore, I orphan this package now.

Maintaining a package requires time and skills. Please only adopt this
package if you will have enough time and attention to work on it.

If you want to be the new maintainer, please see
http://www.debian.org/devel/wnpp/index.html#howto-o for detailed
instructions how to adopt a package properly.

Some information about this package:

Package: otter
Binary: otter, mace2, formed
Version: 3.3f-1.1
Maintainer: Peter Collingbourne <pcc03@doc.ic.ac.uk>
Build-Depends: debhelper (>= 5), libxaw7-dev, hevea
Architecture: any
Standards-Version: 3.7.2
Format: 1.0
Files:
 42be2fcd39cb7b7291e4320fa9bae862 1703 otter_3.3f-1.1.dsc
 795711b307cc1316e08d3d4f46c998c9 2554827 otter_3.3f.orig.tar.gz
 ee42d1cd2f6d1a8bcde108c955d58582 7248 otter_3.3f-1.1.diff.gz
Checksums-Sha1:
 89a6be284d373d7b446d18d551a671335c0dac9a 1703 otter_3.3f-1.1.dsc
 95eef58d733ebb855c0df1d643b6e22246bf3ff2 2554827 otter_3.3f.orig.tar.gz
 591feb6ca422f932b67e073058fed8a798611d5a 7248 otter_3.3f-1.1.diff.gz
Checksums-Sha256:
 2e4130efb6c5dce04b3c21c79b4a673dedfea43feffb04c5ed9eea3314af33fb 1703 otter_3.3f-1.1.dsc
 392c8c6557944eaf6958c199c365b43189beab836fb80c716569ea43af0dac9a 2554827 otter_3.3f.orig.tar.gz
 1ececab9c99a5356183bba32d6f8f22c21a5e1366ed0cff032bc830515c31478 7248 otter_3.3f-1.1.diff.gz
Package-List: 
 formed deb math optional
 mace2 deb math optional
 otter deb math optional
Directory: pool/main/o/otter
Priority: source
Section: math

Package: otter
Version: 3.3f-1.1
Installed-Size: 1289
Maintainer: Peter Collingbourne <pcc03@doc.ic.ac.uk>
Architecture: amd64
Depends: libc6 (>= 2.7)
Recommends: perl, c-shell, mace2
Suggests: formed
Description-en: resolution-style theorem prover
 OTTER is an automated theorem prover for equational logic developed
 at Argonne National Laboratory.
 .
 OTTER's inference rules are based on resolution and paramodulation,
 and it includes facilities for term rewriting, term orderings,
 Knuth-Bendix completion, weighting, and strategies for directing and
 restricting searches for proofs. OTTER can also be used as a symbolic
 calculator and has an embedded equational programming system.
Description-md5: 9377d17015337e1e1d1a0fee8b1cd794
Section: math
Priority: optional
Filename: pool/main/o/otter/otter_3.3f-1.1_amd64.deb
Size: 785362
MD5sum: 2dbebfc4172b694a7ab3cd1b9f814f0c
SHA1: af55b7f320ec75d31cb9b939e5c801d21fa21ef6
SHA256: e93557cc2bf8e895f483e3585776cca13c510b393c4f2ed8cba1d1dd8f8f18f1

Package: mace2
Source: otter
Version: 3.3f-1.1
Installed-Size: 1126
Maintainer: Peter Collingbourne <pcc03@doc.ic.ac.uk>
Architecture: amd64
Depends: libc6 (>= 2.7)
Recommends: perl, c-shell, otter
Suggests: swi-prolog | gprolog
Description-en: program that searches for finite models of first-order statements
 MACE is a program that searches for finite models of first-order and
 equational statements developed at Argonne National Laboratory.
 .
 This package includes ANLDP, which calls the propositional decision
 procedure at the core of MACE directly.
 .
 MACE serves as a complementary companion to OTTER, which
 searches for refutations of the same class of statement. In
 particular, if you have a first-order conjecture, OTTER will search
 for a proof, and MACE will search for a counterexample from the same
 input file.
Description-md5: 3fb8ffe281a2180d32adc0294cc3bc8d
Tag: role::program, use::searching
Section: math
Priority: optional
Filename: pool/main/o/otter/mace2_3.3f-1.1_amd64.deb
Size: 563846
MD5sum: 88b8afb30c1046ad1c1d7d53b88ecc2d
SHA1: 938ce4d51df16402394d17099c2dee40c0ecb0ef
SHA256: 4fb69d996665006ab2f4496ea11e8785019a2290c0801476472431981079adfd

Package: formed
Source: otter
Version: 3.3f-1.1
Installed-Size: 409
Maintainer: Peter Collingbourne <pcc03@doc.ic.ac.uk>
Architecture: amd64
Depends: libc6 (>= 2.7), libx11-6, libxaw7, libxt6
Suggests: otter
Description-en: formula editor for first-order logic formulae
 Formed is a formula editor for first-order logic formulas that
 lets you simplify quantified formulas by quantifier
 transformation among other things.
Description-md5: aa13f669b866573738cbcb8094c4b051
Section: math
Priority: optional
Filename: pool/main/o/otter/formed_3.3f-1.1_amd64.deb
Size: 185652
MD5sum: 5b0746941911d3cbc6ff66d259547bff
SHA1: d97c65a90057d27c983883af9a1e96d7791d04b7
SHA256: e72481f0973f943ecfcd3dc1e5ff5094d4743127569a6a9d763cccd8b3106ecd

[signature.asc (application/pgp-signature, inline)]

Send a report that this bug log contains spam.


Debian bug tracking system administrator <owner@bugs.debian.org>. Last modified: Fri Apr 25 08:34:47 2014; Machine Name: buxtehude.debian.org

Debian Bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.