CMU Artificial Intelligence Repository
Otter: Resolution-based theorem prover.
Otter (Organized Techniques for Theorem-proving and Effective
Research) is a resolution-style theorem-proving program for
first-order logic with equality. Otter includes the inference rules
binary resolution, hyperresolution, UR-resolution, and binary
paramodulation. Some of its other abilities are conversion from
first-order formulas to clauses, forward and back subsumption,
factoring, weighting, answer literals, term ordering, forward and back
demodulation, evaluable functions and predicates, and Knuth-Bendix
Version: 3.0.2 (17-JUN-94); 3.0.1 (PC, 21-FEB-94);
3.0.0 (24-JAN-94); 2.2 (July 1991)
Ports: Unix, Macintosh, IBM PC
Copying: Please send the authors email if you are using the system.
CD-ROM: Prime Time Freeware for AI, Issue 1-1
Author(s): W. McCune
Argonne National Laboratory
Argonne, IL 60438-4844
Answer Literals, Authors!McCune, Automated Reasoning,
Back Demodulation, Back Subsumption, Binary Paramodulation,
Binary Resolution, C!Code, Evaluable Functions,
Evaluable Predicates, Factoring, Forward Demodulation,
Forward Subsumption, Hyperresolution,
Knuth-Bendix Completion, OTTER,
Reasoning!Automated Reasoning, Resolution, Term Ordering,
Theorem Proving, UR-Resolution, Weighting
both propositional and first-order.
anldp100.tgz ANL-DP 1.0.0. Searches for models of sets of clauses,
deduction system", by Lusk and McCune.
presented in "Experiments with ROO, a Parallel Automated
jobs.tgz Input files and Otter output files for experiments
Indexing and Path Indexing for Term Retrieval".
index.tgz Term sets used for "Experiments with Discrimination Tree
unix/ Unix versions (2.2, 3.0.0, 3.0.2)
mac/ Macintosh version
pc/ IBM PC version
A floppy containing the PC version of Otter is included with the new
edition Larry Wos's book, "Automated Reasoning: Introduction and
Applications, McGraw-Hill, 1992".
Last Web update on Mon Feb 13 10:27:38 1995