diff options
| author | zuntum <zuntum@pkgsrc.org> | 2001-11-01 00:32:23 +0000 |
|---|---|---|
| committer | zuntum <zuntum@pkgsrc.org> | 2001-11-01 00:32:23 +0000 |
| commit | 98cf373d367fc32881cb40926be1a79736f39794 (patch) | |
| tree | d0c7515e829b3d20d8e3aaca76db926e459dd4f3 /math/otter/DESCR | |
| parent | a437fd43cc3ece125446142af9ed27ef8c1e6621 (diff) | |
| download | pkgsrc-98cf373d367fc32881cb40926be1a79736f39794.tar.gz | |
Move pkg/ files into package's toplevel directory
Diffstat (limited to 'math/otter/DESCR')
| -rw-r--r-- | math/otter/DESCR | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/math/otter/DESCR b/math/otter/DESCR new file mode 100644 index 00000000000..04f69641f7f --- /dev/null +++ b/math/otter/DESCR @@ -0,0 +1,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. |