The PhD thesis Superposition for Higher-Order Logic by Alexander Bentkamp, which he defended at the VU in May 2021, has received four prestigious awards:
1) The E.W. Beth Dissertation Prize, awarded by the Association for Logic, Language and Information.
2) The Ackermann Award, granted by the European Association for Computer Science Logic.
3) The Bill McCune PhD Award in Automated Reasoning, granted by the Conference on Automated Deduction.
4) The IPA Dissertation Award, granted by the Dutch research school IPA.
His research, which was supervised by Wan Fokkink and Jasmin Blanchette at the VU and by Uwe Waldmann at the Max Planck Institute for Informatics, is dedicated to automatic theorem proving. This means reasoning about logical formulas in order to find proofs of theorems fully automatically.
Alexander developed a so-called higher-order superposition calculus. The prototype Zipperposition tool, to which he contributed substantially, won the higher-order division of the international CASC competition in 2020, 2021, and 2022.