Bibliographic Citation | |
Full Text | |
---|---|
DOI | 10.2172/822573 |
Title | OTTER 3.3 reference manual. |
Creator/Author | McCune, W. |
Publication Date | 2003 Oct 27 |
OSTI Identifier | OSTI ID: 822573 |
Report Number(s) | ANL/MCS-TM-263 |
DOE Contract Number | W-31-109-ENG-38 |
DOI | 10.2172/822573 |
Other Number(s) | TRN: US200413%%295 |
Resource Type | Technical Report |
Resource Relation | Other Information: PBD: 27 Oct 2003 |
Coverage | Topical |
Research Org | Argonne National Lab., IL (US) |
Sponsoring Org | US Department of Energy (US) |
Subject | 99 GENERAL AND MISCELLANEOUS//MATHEMATICS, COMPUTING, AND INFORMATION SCIENCE; O CODES; MANUALS; USES; COMPUTER CALCULATIONS |
Description/Abstract | 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. |
Country of Publication | United States |
Language | English |
Format | Size: 72 pages |
System Entry Date | 2007 Apr 23 |
Document Discussions | |
Top |