Bug#179557: ITP: otter -- Search for proofs in equational logic
Version: N/A; reported 2003-02-03
* Package name : otter
Version : 3.2
Upstream Author : Automated Reasoning Group at Argone National
* URL : http://www.mcs.anl.gov/AR/otter/
* License : available without restriction
Description : Search for proofs in equational logic
The OTTER sources include MACE and FormEd, described below.
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
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: 3.0
Kernel: Linux leonov 2.4.18 #6 Sun Dec 29 08:30:49 CET 2002 i686
Locale: LANG=C, LC_CTYPE=