CMU Artificial Intelligence Repository
Otter: Resolution-based theorem prover.
areas/reasonng/atp/systems/otter/
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
completion.
Origin:
info.mcs.anl.gov:/pub/Otter/Otter-2.2/otter22.tar.Z
anagram.mcs.anl.gov:/pub/Otter/
Version: 3.0.2 (17-JUN-94); 3.0.1 (PC, 21-FEB-94);
3.0.0 (24-JAN-94); 2.2 (July 1991)
Requires: C
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
MCS-221
Argonne National Laboratory
Argonne, IL 60438-4844
Contact: otter@mcs.anl.gov
Keywords:
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
Contains:
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
References:
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
AI.Repository@cs.cmu.edu