OTTER 3.3 Reference Manual

TL;DR

OTTER 3.3 is a comprehensive, portable theorem-proving software for first-order logic with equality, featuring multiple inference rules and advanced proof strategies, implemented in ANSI C for broad accessibility.

Contribution

This manual details OTTER 3.3's extensive features and inference capabilities, enhancing automated theorem proving in first-order logic with equality.

Findings

Supports multiple inference rules including binary resolution and hyperresolution

Includes advanced features like Knuth-Bendix completion and hints strategy

Coded in portable ANSI C for wide compatibility

Abstract

OTTER 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 and features 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, Knuth-Bendix completion, and the hints strategy. OTTER is coded in ANSI C, is free, and is portable to many different kinds of computer.