U.S.-France Cooperative Research: Theory and Applications ofEquational Theorem Proving Techniques based on Completion

9314834 Snyder这个为期三年的奖项支持美国和法国在计算机和计算研究方面的合作研究，由波士顿大学的Wayne Snyder和法国国家科学研究中心信息科学研究中心的Pierre Lescanne以及法国国家信息科学和应用数学研究所（INRIA）共同进行。研究的目的是开发更强大的定理证明程序使用补全和基于调节的技术。他们建议研究波士顿大学和法国开发的调节和完井技术的应用。他们还将负责开发新版本的ORME（法国目前使用的术语重写软件系统）。这个项目利用了法国在术语改写方面的专业知识。这位美国调查人员将使用法国开发的软件ORME来测试他的想法。他为这次合作带来了将定理证明方法与项重写方法相结合的专业知识。所提出的研究将促进类似完井技术在软件工程中的应用。＊＊＊

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. ***