30 November 2022
Postdoc researcher Alexander Bentkamp developed a so-called higher-order superposition calculus. His PhD thesis ‘Superposition for Higher-Order Logic’, which he defended at VU Amsterdam in May 2021, has received four prestigious awards.
Bentkamp’s research, which was supervised by Wan Fokkink and Jasmin Blanchette at VU Amsterdam 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.
With his thesis he received the following awards:
- The E.W. Beth Dissertation Prize, awarded by the Association for Logic, Language and Information.
- The Ackermann Award, granted by the European Association for Computer Science Logic.
- The Bill McCune PhD Award in Automated Reasoning, granted by the Conference on Automated Deduction.
- The IPA Dissertation Award, granted by the Dutch research school IPA.
The prototype Zipperposition tool, to which he contributed substantially, won the higher-order division of the international CASC competition in 2020, 2021, and 2022.