Bibliographic Citation | |
Full Text | |
---|---|
DOI | 10.2172/10129052 |
Title | OTTER 3.0 reference manual and guide |
Creator/Author | McCune, W.W. |
Publication Date | 1994 Jan 01 |
OSTI Identifier | OSTI ID: 10129052; Legacy ID: DE94007457 |
Report Number(s) | ANL--94/6 |
DOE Contract Number | W-31109-ENG-38 |
DOI | 10.2172/10129052 |
Other Number(s) | Other: ON: DE94007457 |
Resource Type | Technical Report |
Resource Relation | Other Information: PBD: Jan 1994 |
Coverage | Topical |
Research Org | Argonne National Lab., IL (United States) |
Sponsoring Org | USDOE, Washington, DC (United States) |
Subject | 99 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 Publication | United States |
Language | English |
Format | Size: 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 Date | 2007 May 07 |
Document Discussions | |
Top |