Dr. Alexander Bentkamp是中科院海外特聘研究助理首批入选者之一，合作导师为软件所詹乃军研究员和詹博华副研究员。由于他博士论文 "Superposition for Higher-Order Logic"的杰出贡献，今年获得三项重要优秀博士论文奖项。 

    国际自动推理联合会（CADE Inc.）与其旗舰会议“自动推理大会”(the Conference on Automated Deduction) 授予他Bill McCune优秀博士奖。该奖项面向全球评选，在定理证明领域每年仅有一人能获此殊荣。此外，国际逻辑、语言与信息学会（FoLLI (the Association for Logic, Language and Information)）授予他E. W. Beth 博士论文奖。荷兰编程与算法研究所 (Institute for Programming research and Algorithmics) 授予他荷兰IPA 博士论文奖。 

    高阶逻辑的自动定理证明长时间以来无人问津，因为许多学者认为一阶逻辑已经足够困难。但近年来，随着基于叠加与可满足性模理论求解的高阶逻辑定理证明器的不断涌现，高阶逻辑逐渐受到研究者的高度重视。Alexander Bentkamp的论文首次将叠加拓展到高阶逻辑中，并证明了这样的拓展是反驳完备的。基于他在论文中提出的演算规则实现的定理证明器 Zipperposition不仅连续两年（2020年和2021年）赢得CADE 自动定理证明系统比赛中的高阶逻辑项目冠军，同时还被整合进著名定理证明器 Isabelle 中，用以实现更高效地构造形式证明。