Otter is an PurpleWiki::InlineNode=HASH(0xa775408)->content developed at the Argonne National Laboratory in Illinois, USA. It is the fourth generation of provers developed there. It was the first widely distributed high-performance theorem prover for [[first-order logic]] with equality, and pioneered a number of important implementation techniques. Otter's inference rules are based on PurpleWiki::InlineNode=HASH(0xa77678c)->content and PurpleWiki::InlineNode=HASH(0xa776834)->content, and it includes facilities for PurpleWiki::InlineNode=HASH(0xa7768dc)->content, PurpleWiki::InlineNode=HASH(0xa776984)->content, [[Knuth-Bendix completion]], PurpleWiki::InlineNode=HASH(0xa776a2c)->content, and strategies for directing and restricting searches for proofs. Otter can also be used as a PurpleWiki::InlineNode=HASH(0xa776ad4)->content and has an embedded PurpleWiki::InlineNode=HASH(0xa777308)->content. (AKY)
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, PurpleWiki::InlineNode=HASH(0xa777578)->content, combinatory logic, group theory, lattice theory, and algebraic geometry. (AKZ)
=== See Also: http://www-unix.mcs.anl.gov/AR/otter/ (AL0)