OTTER 3.3 reference manual.

McCune, W.

Argonne National Laboratory

关键词: Computer Calculations;    Uses;    Manuals;    O Codes;    99 General And Miscellaneous//Mathematics, Computing, And Information Science;   

DOI  :  10.2172/822573
RP-ID  :  ANL/MCS-TM-263
RP-ID  :  W-31-109-ENG-38
RP-ID  :  822573

美国|英语

来源: UNT Digital Library

【 摘 要 】

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.