prover9_0.0.200911a-2.1_amd64.deb


Advertisement

Description

prover9 - theorem prover and countermodel generator

Distribution: Debian 8 (Jessie)
Repository: Debian Main amd64
Package name: prover9
Package version: 0.0.200911a
Package release: 2.1
Package architecture: amd64
Package type: deb
Installed size: 305 B
Download size: 97.58 KB
Official Mirror: ftp.br.debian.org
This package provides the Prover9 resolution/paramodulation theorem prover and 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.

Alternatives

    Download

    Source package: ladr

    Install Howto

    1. Update the package index:
      # sudo apt-get update
    2. Install prover9 deb package:
      # sudo apt-get install prover9

    Files

    • /usr/bin/interpformat
    • /usr/bin/isofilter
    • /usr/bin/isofilter0
    • /usr/bin/isofilter2
    • /usr/bin/mace4
    • /usr/bin/prooftrans
    • /usr/bin/prover9
    • /usr/share/doc/prover9/changelog.Debian.gz
    • /usr/share/doc/prover9/changelog.gz
    • /usr/share/doc/prover9/copyright
    • /usr/share/doc/prover9/examples/mace4.examples/README
    • /usr/share/doc/prover9/examples/mace4.examples/group2.in
    • /usr/share/doc/prover9/examples/mace4.examples/rw1.in
    • /usr/share/doc/prover9/examples/prover9.examples/README
    • /usr/share/doc/prover9/examples/prover9.examples/x2.hints
    • /usr/share/doc/prover9/examples/prover9.examples/x2.in
    • /usr/share/doc/prover9/examples/prover9.examples/x2.out.gz
    • /usr/share/man/man1/interpformat.1.gz
    • /usr/share/man/man1/isofilter.1.gz
    • /usr/share/man/man1/isofilter0.1.gz
    • /usr/share/man/man1/isofilter2.1.gz
    • /usr/share/man/man1/mace4.1.gz
    • /usr/share/man/man1/prooftrans.1.gz
    • /usr/share/man/man1/prover9.1.gz

    Changelog

    2014-10-09 - Matthias Klose <doko@debian.org> ladr (0.0.200911a-2.1) unstable; urgency=medium * Non-maintainer upload. * Build-depend on libtool-bin. Closes: #761761.

    2013-05-25 - Frank Lichtenheld <djpig@debian.org> ladr (0.0.200911a-2) unstable; urgency=low * QA upload. * Upload to unstable. * Change maintainer to QA group.

    2012-12-13 - Hideki Yamane <henrich@debian.org> ladr (0.0.200911a-1) experimental; urgency=low * QA upload. * New upstream release * debian/watch - update to deal with obsolete Perl's regrex (Closes: #544790) Thanks to Adam D. Barratt <adam@adam-barratt.org.uk> * debian/rules - convert to dh7 style - pass "all" to dh_auto_build * debian/patches: convert to use quilt and refresh * debian/source/format: specify "3.0 (quilt)" * debian/control - drop "Build-Depends: dpatch" - remove unnecessary "DM-Upload-Allowed: yes" line - use Multi-Arch - set "Standards-Version: 3.9.4" * debian/compat: set 7 * {libladr4,libladr-dev}.install - adjust install directroy - don't install *.la files - don't install *.so files in -dev package * debian/libladr4.symbols: update

    2012-01-08 - Hideki Yamane <henrich@debian.org> ladr (0.0.200902a-2.1) unstable; urgency=low * Non-maintainer upload. * debian/patches/01-libtoolise.dpatch - it drops -lm but it is needed for binutils-gold (Closes: #555074)

    2009-05-03 - Peter Collingbourne <peter@pcc.me.uk> ladr (0.0.200902a-2) unstable; urgency=low * Merged from Ubuntu, fixes FTBFS (closes: #526541) - Drop -shared from the libtool command to make libladr.la in debian/patches/01-libtoolise.dpatch so that both the shared and static libraries are built. The .install file tries to install both, and if -shared is passed the .a isn't built and the package fails to build. This appears to be a change in libtool behaviour.

    2009-03-14 - Peter Collingbourne <peter@pcc.me.uk> ladr (0.0.200902a-1) unstable; urgency=low * New upstream release. * debian/control: updated for new prover9-doc * debian/ladr4-apps.install, debian/ladr4-apps.links: new application complex, removed application rewriter2 * debian/libladr4.symbols: updated * debian/control: new Standards-Version

    2009-02-17 - Peter Collingbourne <peter@pcc.me.uk> ladr (0.0.200811a-1) unstable; urgency=low * New upstream release. * debian/interpformat.1: documented option "wrap" * debian/patches/01-libtoolise.dpatch: updated from common * debian/libladr4.symbols: updated * debian/control: updated for new prover9-doc * debian/control: Vcs-Bzr uses nosmart+http protocol * debian/clausefilter.1, debian/clausetester.1, debian/control, debian/copyright, debian/interpfilter.1, debian/interpformat.1, debian/isofilter.1, debian/ladr4-apps.1, debian/ladr4-apps.README.Debian, debian/mace4.1, debian/prooftrans.1, debian/prover9.1, debian/rewriter.1: changed maintainer email address (again) * debian/ladr4-apps.install, debian/ladr4-apps.links: new application rewriter2 * debian/control: do not duplicate "Section" field for binary packages * debian/copyright: changed year to 2009, corrected expression of copyright, refer to GPL-2 explicitly

    2008-09-13 - Peter Collingbourne <peter@peter.uk.to> ladr (0.0.200809a-1) unstable; urgency=low * New upstream release. * debian/patches/01-libtoolise.dpatch: new programmatic patch script, original version by Heinz Wiesinger <pprkut@liwjatan.at> * debian/control: updated for new prover9-doc * debian/libladr4.symbols: updated * debian/clausefilter.1, debian/clausetester.1, debian/control, debian/copyright, debian/interpfilter.1, debian/interpformat.1, debian/isofilter.1, debian/ladr4-apps.1, debian/ladr4-apps.README.Debian, debian/mace4.1, debian/prooftrans.1, debian/prover9.1, debian/rewriter.1: changed maintainer email address

    Advertisement
    Advertisement