diff options
Diffstat (limited to 'math/otter/DESCR')
| -rw-r--r-- | math/otter/DESCR | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/math/otter/DESCR b/math/otter/DESCR deleted file mode 100644 index 04f69641f7f..00000000000 --- a/math/otter/DESCR +++ /dev/null @@ -1,10 +0,0 @@ -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. |