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

点击翻译按钮获取中文摘要

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.