last modified: 03-MAY-2001 | catalog | categories | new | search |

NESC9469 OTTER.

OTTER, Resolution Style Theorem Prover

top ]
1. NAME OR DESIGNATION OF PROGRAM:  OTTER.
top ]
2. COMPUTERS
To submit a request, click below on the link of the version you wish to order. Only liaison officers are authorised to submit online requests. Rules for requesters are available here.
Program name Package id Status Status date
OTTER NESC9469/01 Arrived 03-MAY-2001

Machines used:

Package ID Orig. computer Test computer
NESC9469/01 IBM PC
top ]
3. DESCRIPTION OF PROGRAM OR FUNCTION

OTTER (Other 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. These inference rules take as small set of clauses and infer a clause. If the inferred clause is new and useful, it is stored and may become available for subsequent inferences. Other capabilities are conversion from first-order formulas to clauses, forward and back subsumption, factoring, weighting, answer literals, term ordering, forward and back demodulation, and evaluable functions and predicates.
top ]
4. METHOD OF SOLUTION

For its inference process OTTER uses the given-clause algorithm, which can be viewed as a simple implementation of the set of support strategy. OTTER maintains three lists of clauses: axioms, sos (set of support), and demodulators.
OTTER is not automatic. Even after the user has encoded a problem into first-order logic or into clauses, the user must choose inference rules, set options to control the processing of inferred clauses, and decide which input formulae or clauses are to be in the initial set of support and which, if any, equalities are to be demodulators. If OTTER fails to find a proof, the user may try again different initial conditions.
top ]
5. RESTRICTIONS ON THE COMPLEXITY OF THE PROBLEM

Maxima of -
   5000 characters in an input string
     64 distinct variables in a clause
     51 characters in any symbol
The maxima can be changed by finding the appropriate definition (#define) in the header.h file, increasing the limit, and recompiling OTTER.
   There are a few constraints on the order of commands.
top ]
6. TYPICAL RUNNING TIME:
top ]
7. UNUSUAL FEATURES OF THE PROGRAM:
top ]
8. RELATED AND AUXILIARY PROGRAMS

OTTER is similar in scope and purpose to the AURA and LMA,ITP (NESC 9828) theorem provers.
top ]
9. STATUS
Package ID Status date Status
NESC9469/01 03-MAY-2001 Masterfiled Arrived
top ]
10. REFERENCES

- OTTER, NESC No. 9469.MPLN, OTTER Berkeley UNIX Version Tape
  Directory,
  National Energy Software Center Note 89-85, August 28, 1989.
- L. Wos, R. Overleek, E. Lusk, and J. Boyle
  Automated Reasoning: Introduction and Applications
  Prentice-Hall, Englewood Cliffs, New Jersey, 1984.
NESC9469/01, included references:
- W.W. McCune:
  OTTER 1.0 User's Guide
  ANL-88-44 (January 1989)
- M. Birgersson:
  OTTER IBM PC/AT Flexible Disk Cartridge Directories
  NESC Notes 89-86 (August 28, 1989)
top ]
11. MACHINE REQUIREMENTS

Any computer using a Berkeley UNIX operating  system or an IBM PC/AT or compatible system.
top ]
12. PROGRAMMING LANGUAGE(S) USED
Package ID Computer language
NESC9469/01 FORTRAN+C
top ]
13. OPERATING SYSTEM UNDER WHICH PROGRAM IS EXECUTED:  Berkeley UNIX (MPLN), MS-DOS (IBM PC/AT).
top ]
14. OTHER PROGRAMMING OR OPERATING INFORMATION OR RESTRICTIONS:
top ]
15. NAME AND ESTABLISHMENT OF AUTHORS

          W.W. McCune
          Mathematics and Computer Science Division
          Argonne National Laboratory
top ]
16. MATERIAL AVAILABLE
NESC9469/01
source program   mag tapeOTTER Source Program                       SRCTP
test-case data   mag tapeControl Information                        DATTP
load module      mag tapeExecutable Image                           LODTP
test-case data   mag tapeSample Problem Input                       DATTP
test-case output mag tapeSample Problem Output                      OUTTP
report                   ANL-88-44 (January 1989)                   REPPT
prog. note               NESC Notes 89-86 (August 28, 1989)         NOTPT
top ]
17. CATEGORIES
  • P. General Mathematical and Computing System Routines

Keywords: mathematical logic.