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 ---
- To: Debian Bug Tracking System <submit@bugs.debian.org>
- Subject: ITP: ladr -- deduction library, theorem prover and countermodel generator
- From: Peter Collingbourne <pcc03@doc.ic.ac.uk>
- Date: Tue, 14 Aug 2007 22:22:49 +0100
- Message-id: <20070814212248.11269.72477.reportbug@lappy.peter.uk.to>
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: