2003/10/28 by William McCune, McCune, William · 2 citations
Computer Science · #F.4.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Mathematical Software (cs.MS) #Model-Driven Software Engineering Techniques #Symbolic Computation (cs.SC) #cs.MS #cs.SC
paper · pdf · doi:10.48550/arxiv.cs/0310056
66 pages
arxiv created 2003/10/28 · openalex publication_date 2003/10/28 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.