In both mathematics and logic, many theorems exist such that each can be proved in entirely different ways. For a striking example, there exist theorems from group theory that can be proved by relying solely on equality and (from the viewpoint of automated reasoning) the use of paramodulation, but can also be proved in a notation in which equality is totally absent and the inference rule is condensed detachment (captured with a single clause and the rule hyper-resolution). A study of such examples immediately shows how far from obvious is the problem of producing a proof in one system even in the presence of a proof in another; such problems can be viewed as ones of translation, where the rules of translation and the translation itself are frequently difficult to obtain. In this report, we discuss in detail various techniques that can be applied by the automated reasoning program OTTER to address the translation problem to obtain a proof in one notation and inference system given a proof in a completely different notation and inference system. To illustrate the techniques, we present a full treatment culminating in a successful translation'' of a proof of a theorem from many-valued sentential calculus. …

The COMMIX-PPC computer program is an extended and improved version of earlier COMMIX codes and is specifically designed for evaluating the thermal performance of power plant condensers. The COMMIX codes are general-purpose computer programs for the analysis of fluid flow and heat transfer in complex industrial systems. In COMMIX-PPC, two major features have been added to previously published COMMIX codes. One feature is the incorporation of one-dimensional conservation of mass, momentum, and energy equations on the tube side, and the proper accounting for the thermal interaction between shell and tube side through the porous medium approach. The other added feature is the extension of the three-dimensional conservation equations for shell-side flow to treat the flow of a multicomponent medium. COMMIX-PPC is designed to perform steady-state and transient three-dimensional analysis of fluid flow with heat transfer in a power plant condenser. However, the code is designed in a generalized fashion so that, with some modification, it can be used to analyze processes in any heat exchanger or other single-phase engineering applications.

Abstract: This is the history of the Institute for Numerical Analysis (INA) with special emphasis in its research program during the period 1947 to 1956. The Institute for Numerical Analysis was located on the campus of the University of California, Los Angeles. It was a section of the National Applied Mathematics Laboratories, which formed the Applied Mathematics Division of the National Bureau of Standards (now the National Institute of Standards and technology), under the U.S. Department of Commerce.

Progress report of the Argonne National Laboratory's Nuclear Technology Programs involving R&D in three areas: applied physical chemistry, separation science and technology, and nuclear waste management.

This report reviews the research activities in the Mathematics and Computer Science Division at Argonne National Laboratory for the period September 1989 through February 1991. The body of the report gives a brief look at the MCS staff and the research facilities and then discusses the diverse research projects carried out in the division. Projects funded by non-DOE sources are also discussed, and new technology transfer activities are described. Further information on staff, visitors, workshops, and seminars is found in the appendixes.

This is a description of and a user's manual for upshot, an X-based graphics tool for viewing log files produced by parallel programs.