OTTER 3.3 Reference Manual
OTTER 3.3 Reference Manual
复制标题
OTTER 3.3 参考手册
DOI：
10.2172/822573
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
["W. McCune
中科院分区：
文献类型：
--
作者：
["W. McCune
OTTER 是一个用于一阶逻辑等式的解析式定理证明程序。 OTTER 包括二进制分辨率、超分辨率、UR 分辨率和二进制参数调制的推理规则。它的一些其他功能和特性包括从一阶公式到子句的转换、前向和后向包含、因式分解、加权、答案文字、术语排序、前向和后向解调、可评估函数和谓词、Knuth-Bendix 完成和提示策略。 OTTER 采用 ANSI C 编码，免费，并且可移植到许多不同类型的计算机。
OTTER 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, Knuth-Bendix completion, and the hints strategy. OTTER is coded in ANSI C, is free, and is portable to many different kinds of computer.