Information Bridge

Bibliographic Citation 
Full Text PDF 4 Mb   View Full Text or Access Individual Pages  -   search, view and/or download individual pages
DOI 10.2172/10129052
Title OTTER 3.0 reference manual and guide
Creator/Author McCune, W.W.
Publication Date1994 Jan 01
OSTI IdentifierOSTI ID: 10129052; Legacy ID: DE94007457
Report Number(s)ANL--94/6
DOE Contract NumberW-31109-ENG-38
DOI10.2172/10129052
Other Number(s)Other: ON: DE94007457
Resource TypeTechnical Report
Resource RelationOther Information: PBD: Jan 1994
CoverageTopical
Research OrgArgonne National Lab., IL (United States)
Sponsoring OrgUSDOE, Washington, DC (United States)
Subject99 GENERAL AND MISCELLANEOUS//MATHEMATICS, COMPUTING, AND INFORMATION SCIENCE; MATHEMATICAL LOGIC; O CODES; CALCULATION METHODS; MANUALS; ARTIFICIAL INTELLIGENCE
Description/Abstract 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.
Country of PublicationUnited States
LanguageEnglish
FormatSize: 58 p.
Availability OSTI as DE94007457; Paper copy available at OSTI: phone, 865-576-8401, or email, reports@adonis.osti.gov
To purchase this media from NTIS, click here
System Entry Date2007 May 07
Document Discussions
 (for display)
 (Email address will NOT be displayed.)

   (All fields required. Document Discussions not displayed until approved.)

Top