blob: 04f69641f7f7209037264c0e15ab63bcfe9bd6cb (
plain)
1
2
3
4
5
6
7
8
9
10
|
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.
|
