9314834 Snyder This three-year award supports U.S.-France cooperative research in computer and computation research between Wayne Snyder, Boston University and Pierre Lescanne of the CNRS' Center for Research in Information Sciences and INRIA (The French National Institute for Information Sciences and Applied Mathematics). The objective of the research is to develop more powerful theorem proving programs using completion and paramodulation-based techniques. They propose to investigate applications of paramodulation and completion developed at Boston University and in France. They will also undertake the development of a new version of ORME (a term-rewriting software system currently used in France). This project takes advantage of French expertise in term- rewriting. The U.S. investigator will use the French developed software, ORME, for testing his ideas. He brings to this collaboration expertise in integrating methods of theorem proving with those of term-rewriting. The proposed research will advance the use of completion-like techniques in software engineering. ***
