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

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

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)

Reply to: