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, URresolution, and binary paramodulation. Some of its other abilities 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, it is free, and it is portable to many different kinds of computers.

Highlights of the Chemical Technology (CMT) Division's activities during 1989 are presented. In this period, CMT conducted research and development in the following areas: (1) electrochemical technology, including high-performance batteries (mainly lithium/iron sulfide and sodium/metal chloride), aqueous batteries (lead-acid and nickel/iron), and advanced fuel cells with molten carbonate and solid oxide electrolytes; (2) coal utilization, including the heat and seed recovery technology for coal-fired magnetohydrodynamics plants and the technology for fluidized-bed combustion; (3) method, for recovery of energy from municipal waste and techniques for treatment of hazardous organic waste; (4) nuclear technology related to a process for separating and recovering transuranic elements from nuclear waste and for producing 99Mo from low-enriched uranium targets, the recovery processes for discharged fuel and the uranium blanket in a sodium-cooled fast reactor (the Integral Fast Reactor), and waste management; and (5) physical chemistry of selected materials in environments simulating those of fission and fusion energy systems.