International Postdoctoral Fellows Program: A Transformation-Based Order-Sorted Higher-Order Unification Algorithm in Combinatory Logic

该奖项是根据国际博士后研究员计划颁发的，该计划使美国科学家和工程师能够在国外公认的卓越研究中心进行为期3至12个月的研究。该项目的奖项提供了联合研究的机会，并提供了使用国外独特或互补的设施、专业知识和实验条件的机会。这一奖项将支持帕特里夏·约翰博士对萨尔兰兹大学为期八个月的博士后研究访问，与约格·西克曼博士合作。他们建议开发和监督一个完整的基于转换的统一算法的实现，该算法适用于用组合逻辑表示的高阶逻辑，并受带有术语声明的全顺序排序类型结构的约束。他们的算法将包括首次排序的高阶归结定理证明器MRKP的一个重要组成部分，萨尔布吕肯的西克曼博士和卡内基梅隆大学的彼得·安德鲁斯博士的研究小组正在建设中。该奖项建议为八个月的津贴提供资金。

This award is under the International Postdoctoral Fellows Program, which enables U.S. scientists and engineers to conduct three to twelve months of research abroad at research centers of proven excellence. The program's awards provide opportunities for joint research, and the use of unique or complementary facilities, expertise and experimental conditions abroad. This award will support an eight-month postdoctoral research visit by Dr. Patricia Johann to the University of Saarlands to work with Dr. Jorg Siekmann. They propose to develop and oversee the implementation of a complete transformation- based unification algorithm for higher-order logic expressed in terms of combinatory logic and subject to the constraints of a full order- sorted type structure with term declarations. Their algorithm will comprise an important component of the first-ever order-sorted higher-order resolution theorem prover, MRKP, under construction by the research groups of Dr. Siekmann in Saarbrucken and Dr. Peter Andrews at Carnegie Mellon University. The award recommendation provides funds for a stipend for eight months.