11 lines
628 B
Text
11 lines
628 B
Text
|
Otter (Organized Techniques for Theorem-proving and Effective
|
||
|
|
Research) is a resolution-style theorem-proving program for
|
||
|
|
first-order logic with equality. Otter includes the inference rules
|
||
|
|
binary resolution, hyperresolution, UR-resolution, and binary
|
||
|
|
paramodulation. Some of its other abilities and features are
|
||
|
|
conversion from first-order formulas to clauses, forward and back
|
||
|
|
subsumption, factoring, weighting, answer literals, term ordering,
|
||
|
|
forward and back demodulation, evaluable functions and predicates, and
|
||
|
|
Knuth-Bendix completion. Otter is coded in C, is free, and is
|
||
|
|
portable to many different kinds of computer.
|