Bug#397257: ITP: otter -- resolution-style theorem prover

[Peter Collingbourne <pcc03@doc.ic.ac.uk>]

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)