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 中，用以實現更高效地構造形式證明。