CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

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