Dr. Alexander Bentkamp, whose supervisor is Prof. ZHAN Naijun from Institute of Software Chinese Academy of Sciences (ISCAS), is one of the first winners of CAS scholarship for outstanding oversea PhD. In this year, he won three awards for his PhD thesis Superposition for Higher-Order Logic: the Bill McCune PhD Award from CADE Inc., the Conference on Automated Deduction on August 10, the E. W. Beth Dissertation Prize from the Association for Logic, Language and Information (FoLLI) on August 12. and the IPA Dissertation Award from the Institute for Programming Research and Algorithmics on October 3.

For many years, automated theorem proving in higher-order logic was something of a fringe topic. In recent years, the picture has changed dramatically with the emergence of higher-order provers based on superposition and satisfiability-modulo-theories solvers. Alexander's thesis played a key role in this breakthrough. This work presented in his thesis pioneered the idea that superposition can be extended to higher-order logic and such extended superpostion can be refutationally completed. Based on the implement of the new calculus presented in Alexander's thesis, the prover Zipperposition not only has won the Higher-order Division of the yearly CADE ATP System Competition in 2020 and 2021, but also has been integrated into the proof assis-tant Isabelle, helping its users to construct formal proofs more efficiently.