The primary objective of automated reasoning is to develop computer programs that will help people solve problems requiring logical reasoning. Such programs already have been used successfully in several application areas, including, for example, solving open questions in mathematics and solving a variety of verification and design problems. Our research efforts in automated reasoning focus on the development of the underlying theory, the development of software that will provide a wide variety of problem-solving capabilities, and the development of a metatheory for using the software in the most effective way. We also are interested in the application of automated reasoning to a variety of problem domains.
