Otter

Abstract

Our current automated deduction system Otter is designed to prove theorems stated in first-order logic with equality. Otter's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs. Otter can also be us ed as a symbolic calculator and has an embedded equational programming syst em. Currently, the main application of Otter is research in abstract algebra and formal logic. Otter and its predecessors have been used to answer many open questions in the areas of finite semigroups, ternary Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry. Otter has also been used for research in the verification of hardware and software.

DateOfInformation

Fri Feb 5 16:28:04 1999

Domain

Scientific and Engineering Applications

Name

Otter

TargetEnvironment

Otter is coded in C and is portable, simple to install, and very fast. It has been used mostly on UNIX systems, but limited versions (included in the distribution) also run on PCs and Macintoshes.

Webpage

http://www.mcs.anl.gov/AR/otter/

ContactIs

William McCune