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

Bug#437936: marked as done (ITP: ladr -- deduction library, theorem prover and countermodel generator)



Your message dated Sat, 09 Feb 2008 16:21:40 +0000
with message-id <E1JNsSS-00005d-KJ@ries.debian.org>
and subject line Bug#437936: fixed in ladr 0.0.200712-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    : ladr
  Version         : 0.0.200708
  Upstream Author : William McCune <mccune@cs.unm.edu>
* URL             : http://www.cs.unm.edu/~mccune/mace4/
* License         : GPL
  Programming Lang: C
  Description     : deduction library, theorem prover and countermodel generator

 The source package ladr includes the LADR deduction library, along
 with the prover9 theorem prover, the mace4 countermodel generator and
 a number of related applications.

 LADR is a library for use in constructing theorem provers.  Among other
 useful routines it provides facilities for applying inference rules
 such as resolution and paramodulation to clauses.  LADR is used by the
 prover9 theorem prover, and by the mace4 countermodel generator.

 Prover9 is an automated theorem prover for first-order and equational
 logic. It is a successor of the Otter prover.  Prover9 uses the
 inference techniques of ordered resolution and paramodulation with
 literal selection.

 The program Mace4 searches for finite structures satisfying first-order
 and equational statements, the same kind of statement that Prover9
 accepts. If the statement is the denial of some conjecture, any
 structures found by Mace4 are counterexamples to the conjecture.
 .
 Mace4 can be a valuable complement to Prover9, looking for
 counterexamples before (or at the same time as) using Prover9 to search
 for a proof. It can also be used to help debug input clauses and formulas
 for Prover9.

-- System Information:
Debian Release: lenny/sid
  APT prefers testing
  APT policy: (500, 'testing')
Architecture: i386 (i686)

Kernel: Linux 2.6.15-1-686
Locale: LANG=en_GB.UTF-8, LC_CTYPE=en_GB.UTF-8 (charmap=UTF-8)
Shell: /bin/sh linked to /bin/bash


--- End Message ---
--- Begin Message ---
Source: ladr
Source-Version: 0.0.200712-1

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

ladr4-apps_0.0.200712-1_i386.deb
  to pool/main/l/ladr/ladr4-apps_0.0.200712-1_i386.deb
ladr_0.0.200712-1.diff.gz
  to pool/main/l/ladr/ladr_0.0.200712-1.diff.gz
ladr_0.0.200712-1.dsc
  to pool/main/l/ladr/ladr_0.0.200712-1.dsc
ladr_0.0.200712.orig.tar.gz
  to pool/main/l/ladr/ladr_0.0.200712.orig.tar.gz
libladr-dev_0.0.200712-1_i386.deb
  to pool/main/l/ladr/libladr-dev_0.0.200712-1_i386.deb
libladr4_0.0.200712-1_i386.deb
  to pool/main/l/ladr/libladr4_0.0.200712-1_i386.deb
prover9_0.0.200712-1_i386.deb
  to pool/main/l/ladr/prover9_0.0.200712-1_i386.deb



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 437936@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 ladr 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: Tue, 22 Jan 2008 17:39:05 +0000
Source: ladr
Binary: libladr-dev libladr4 prover9 ladr4-apps
Architecture: source i386
Version: 0.0.200712-1
Distribution: unstable
Urgency: low
Maintainer: Peter Collingbourne <pcc03@doc.ic.ac.uk>
Changed-By: Peter Collingbourne <pcc03@doc.ic.ac.uk>
Description: 
 ladr4-apps - the LADR deduction library, miscellaneous applications
 libladr-dev - the LADR deduction library, development files
 libladr4   - the LADR deduction library
 prover9    - theorem prover and countermodel generator
Closes: 437936
Changes: 
 ladr (0.0.200712-1) unstable; urgency=low
 .
   * Initial release (Closes: #437936)
   * Fixed and libtoolized Makefiles
   * Wrote man pages
   * utilities/get_givens, utilities/get_interps, utilities/get_kept:
     now use Bourne shell to avoid unneccessary dependencies
Files: 
 5a698c766b64072234503edba439e5cf 730 math optional ladr_0.0.200712-1.dsc
 6e2896ed4cce4556bfcc321778df5dfe 1787225 math optional ladr_0.0.200712.orig.tar.gz
 d1534198bae410f26aa02e2a848231df 20485 math optional ladr_0.0.200712-1.diff.gz
 cc4434b9e2fff47f7a6d231297413cfa 325370 libdevel optional libladr-dev_0.0.200712-1_i386.deb
 7457577278dd42e51be68b153614f936 196470 libs optional libladr4_0.0.200712-1_i386.deb
 351bd1195fb7684cda2748da62a97062 104344 math optional prover9_0.0.200712-1_i386.deb
 d38a5202290ddf83a779dee0b1c4cb1f 302986 math optional ladr4-apps_0.0.200712-1_i386.deb

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

iD8DBQFHp1c9BnqtBMk7/3kRAmkJAKCo8e7Dy+Bf22UoukmAx6938XhCsACfW9rT
mn7K4l972xOtgTi+EQW50/Q=
=e+tk
-----END PGP SIGNATURE-----



--- End Message ---

Reply to: