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

该奖项是根据国际 博士后研究员计划，使 美国科学家和工程师将进行三次 在国外进行为期12个月的研究 卓越的中心。 该计划的 奖项提供机会， 研究，以及使用独特或 配套设施、专业知识和 国外的实验条件。 该奖项将支持为期八个月的 Patricia博士的博士后研究访问 约翰到萨尔大学工作 约格·西克曼医生的 他们建议制定和监督 实现全面转型- 高阶统一算法 用组合逻辑表示的逻辑 并在一项全面命令的规限下─ 带术语声明的排序类型结构。 他们的算法将包含一个重要的 第一个有序的组成部分 高阶分辨定理证明器 正在建设中的研究小组， 萨尔布吕肯的西克曼医生和彼得医生 卡内基梅隆大学的安德鲁。 授标建议提供资金， 八个月的津贴。

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.