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

小行星9314834 这个为期三年的奖项支持美国-法国波士顿大学韦恩·斯奈德和法国国家科学研究中心信息科学研究中心的皮埃尔·莱斯坎内以及法国国家信息科学和应用数学研究所在计算机和计算研究方面的合作研究。 研究的目的是开发更强大的定理证明程序使用完成和paramodulation-based技术。 他们建议调查的应用paramodulation和完成开发在波士顿大学和法国。 他们还将开发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. ***