Bibliographic Citation
See/Add Document Discussions Return to Search Results Return to Original Search Page Download as EndNote
Full Text	0 K   View Full Text or Access Individual Pages  -   search, view and/or download individual pages
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 Discuss	User Name:  (for display) Email Address:  (Email address will NOT be displayed.) Discussion Subject:    (All fields required. Document Discussions not displayed until approved.)
See/Add Document Discussions Return to Search Results Return to Original Search Page Download as EndNote
Top