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: