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

Bug#397257: marked as done (ITP: otter -- resolution-style theorem prover)

Your message dated Sat, 27 Jan 2007 15:31:27 +0000
with message-id <E1HApWZ-0007JY-B3@ries.debian.org>
and subject line Bug#397257: fixed in otter 3.3f-1
has caused the attached Bug report to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what I am
talking about this indicates a serious mail system misconfiguration
somewhere.  Please contact me immediately.)

Debian bug tracking system administrator
(administrator, Debian Bugs database)
--- Begin Message --- 
Package: wnpp
Severity: wishlist
Owner: Peter Collingbourne <pcc03@doc.ic.ac.uk>


* Package name    : otter
  Version         : 3.3f
  Upstream Author : William McCune <otter@mcs.anl.gov>
* URL             : http://www.cs.unm.edu/~mccune/otter/
* License         : public domain
  Programming Lang: C
  Description     : 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.

 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.

 Formed is a formula editor for first-order logic formulas that
 lets you simplify quantified formulas by quantifier
 transformation among other things.

-- System Information:
Debian Release: testing/unstable
  APT prefers testing
  APT policy: (500, 'testing')
Architecture: i386 (i686)
Shell:  /bin/sh linked to /bin/bash
Kernel: Linux 2.6.17-2-686
Locale: LANG=en_GB, LC_CTYPE=en_GB (charmap=ISO-8859-1)

--- End Message ---
--- Begin Message --- 
Source: otter
Source-Version: 3.3f-1

We believe that the bug you reported is fixed in the latest version of
otter, which is due to be installed in the Debian FTP archive:

formed_3.3f-1_i386.deb
  to pool/main/o/otter/formed_3.3f-1_i386.deb
mace2_3.3f-1_i386.deb
  to pool/main/o/otter/mace2_3.3f-1_i386.deb
otter_3.3f-1.diff.gz
  to pool/main/o/otter/otter_3.3f-1.diff.gz
otter_3.3f-1.dsc
  to pool/main/o/otter/otter_3.3f-1.dsc
otter_3.3f-1_i386.deb
  to pool/main/o/otter/otter_3.3f-1_i386.deb
otter_3.3f.orig.tar.gz
  to pool/main/o/otter/otter_3.3f.orig.tar.gz



A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 397257@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Peter Collingbourne <pcc03@doc.ic.ac.uk> (supplier of updated otter package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@debian.org)


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Format: 1.7
Date: Sun,  5 Nov 2006 22:42:36 +0000
Source: otter
Binary: otter mace2 formed
Architecture: source i386
Version: 3.3f-1
Distribution: unstable
Urgency: low
Maintainer: Peter Collingbourne <pcc03@doc.ic.ac.uk>
Changed-By: Peter Collingbourne <pcc03@doc.ic.ac.uk>
Description: 
 formed     - formula editor for first-order logic formulae
 mace2      - program that searches for finite models of first-order statements
 otter      - resolution-style theorem prover
Closes: 397257
Changes: 
 otter (3.3f-1) unstable; urgency=low
 .
   * Initial release (Closes: #397257)
   * Fixed broken Makefiles
   * Wrote manpages
   * examples/Loop/otter-ploop, examples/summary: Fixed broken
     interpreter path
Files: 
 28b271b45c5825e05504d7e5578591bc 589 math optional otter_3.3f-1.dsc
 795711b307cc1316e08d3d4f46c998c9 2554827 math optional otter_3.3f.orig.tar.gz
 c882f71fa5e5d8e2cd444de216cc9cf6 7134 math optional otter_3.3f-1.diff.gz
 55bdee9ce191c3cbe86f71cc2183257a 761570 math optional otter_3.3f-1_i386.deb
 758314d19e96d3ca22305f74fd1d30b0 508304 math optional mace2_3.3f-1_i386.deb
 ccc52c5fe91ed06ee18ddfc881c7f9fb 157358 math optional formed_3.3f-1_i386.deb

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)

iD8DBQFFnCH2+C5cwEsrK54RAnULAJsEIO0xX39Hb2swhqxUA2CsC3q2pwCgurkF
PyqzNg1JRPfnL/6CdV6/JkM=
=Ipw4
-----END PGP SIGNATURE-----

--- End Message ---
Reply to: