Otter is a
problem solver computer system (also described as an
automated deduction system), suited to solving
logical and
algebraic problems. A description from the Otter website:
"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...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."
It works by taking a list of axioms and a hypothesis; Otter then works to try and find a pair of axioms, or an axiom and hypothesis which are mutually exclusive, by using logical steps. Otter then spits out a proof which effectively shows that one of the two statements in your input is wrong.
Otter has a good few predecessors from the sixties and seventies. It and its current relatives EQP and MACE have discovered a few interesting new results, such as proof of the Robbins conjecture. The latest versions of Otter are available to download from the Otter website, and come packaged with MACE.
A bit more information is available at http://www-unix.mcs.anl.gov/AR/otter/#description