NESC9469 OTTER.
OTTER, Resolution Style Theorem Prover
NAME OR DESIGNATION OF PROGRAM, COMPUTER, DESCRIPTION OF PROGRAM OR FUNCTION, METHOD OF SOLUTION, RESTRICTIONS ON THE COMPLEXITY OF THE PROBLEM, TYPICAL RUNNING TIME, UNUSUAL FEATURES OF THE PROGRAM, RELATED AND AUXILIARY PROGRAMS, STATUS, REFERENCES, MACHINE REQUIREMENTS, LANGUAGE, OPERATING SYSTEM UNDER WHICH PROGRAM IS EXECUTED, OTHER PROGRAMMING OR OPERATING INFORMATION OR RESTRICTIONS, NAME AND ESTABLISHMENT OF AUTHORS, MATERIAL, CATEGORIES
[ top ]
[ top ]
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.
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.
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.
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 ]
[ top ]
[ top ]
[ 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.
- 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 ]
[ top ]
[ top ]
[ top ]
[ top ]
NESC9469/01
source program mag tapeOTTER Source Program SRCTPtest-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
Keywords: mathematical logic.