resolution-style theorem prover
OTTER is an automated theorem prover for equational logic developed
at Argonne National Laboratory.
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 used as a symbolic
calculator and has an embedded equational programming system.
Generated by Doxygen 1.6.0 Back to index