9315241 Hoover This award supports collaboration between Douglas Hoover, Odyssey Research Associates, Inc., Ithaca, New York, and Wang Ju, Software Institute, Chinese Academy of Sciences, Beijing, China, on simplification of generalized arithmetic formulas. The US PI will spend five months in China at the Software Institute working with a group of Chinese mathematical logicians on applications of logic to computer science, including theorem proving. This will be followed by a visit of two Chinese scientists to the US to continue the work. The proposed research falls in the area of theoretical computer science, specifically automatic theorem proving. The US PI and his institution, ORA, are leading specialists in this are a of research and the Chinese Academy of Sciences' Institute of Software is the leading site for such research in China. The work proposed is necessary if automated reasoning techniques are to become feasible tools for computer-aided design. Once such tools become practical, the effect on design will be potentially revolutionary.
