Logo Search packages:      
Sourcecode: otter version File versions  Download package

otter Documentation

3.3f-1

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