OTTER 3.3 Reference Manual

Simple item page
dc.creatorMcCune, William
dc.date2003-10-28
dc.date.accessioned2026-07-07T03:20:31Z
dc.date.available2026-07-07T03:20:31Z
dc.descriptionOTTER 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.
dc.description66 pages
dc.identifierhttps://arxiv.org/abs/cs/0310056
dc.identifierhttp://arxiv.org/abs/cs/0310056
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/31851
dc.subjectSymbolic Computation
dc.subjectMathematical Software
dc.subjectF.4.1
dc.titleOTTER 3.3 Reference Manual
dc.typetext

Files

Collections

arXiv