I am a postdoctoral researcher in the Theoretical Computer Science section of the Vrije Universiteit Amsterdam, Netherlands. My main research interests are automated and interactive theorem proving. I am part of the Matryoshka project, where I work on a superposition calculus for higher-order logic. I have a PhD in computer science from the Vrije Universiteit Amsterdam. Before my PhD, I studied mathematics and computational linguistics.
Zipperposition achieved first place in the higher-order division of the prover competition CASC 2020.
CASC website
Efficient full higher-order unification
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin.
Draft article (PDF)
The Embedding Path Order for Lambda-Free Higher-Order Terms
Alexander Bentkamp.
Draft article (PDF) ⋅
Supplementary material ⋅
Slides (PDF)
Superposition for full higher-order logic
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović.
In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28),
LNCS, Springer, 2021.
Authors' PDF ⋅
Report (PDF)
Superposition with first-class Booleans and inprocessing clausification
Visa Nummelin, Alexander Bentkamp, Sophie Tourret, and Petar Vukmirović.
In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28),
LNCS, Springer, 2021.
Authors' PDF ⋅
Report (PDF)
Making Higher-Order Superposition Work
Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret.
In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28),
LNCS, Springer, 2021.
Authors' PDF
Superposition with lambdas
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann.
Accepted in Journal of Automated Reasoning.
Authors' PDF ⋅
Supplementary material
Superposition for lambda-free higher-order logic
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann.
Logical Methods in Computer Science 17(2): 1:1–1:38, 2021.
Publisher's page ⋅
Authors' PDF ⋅
Supplementary material
Efficient full higher-order unification
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin.
In Ariola, Z.M. (ed.), 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020),
LIPIcs 167, pp. 5:1–5:17, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2020.
Publisher's page ⋅
Authors' PDF ⋅
Report (PDF)
Superposition with lambdas
Alexander Bentkamp, Jasmin Christian Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann.
In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27),
LNCS 11716, pp. 55–73, Springer, 2019.
Publisher's page ⋅
Authors' PDF ⋅
Report (PDF) ⋅
Slides (PDF)
A formal proof of the expressiveness of deep learning
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. Journal of Automated Reasoning 63(2), pp. 347-368, 2019.
Publisher's page ⋅
Authors' PDF
Superposition for lambda-free higher-order logic
Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, and Uwe Waldmann.
In Galmiche, D., Schulz, S., Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning (IJCAR 2018),
LNCS 10900, pp. 28–46, Springer, 2018.
Publisher's page ⋅
Authors' PDF ⋅
Report (PDF) ⋅
Slides (PDF) ⋅
Supplementary material
A formal proof of the expressiveness of deep learning
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow.
In Ayala-Rincón, M., Muños, C. A. (eds.) 8th Conference on Interactive Theorem Proving (ITP 2017),
LNCS 10499, pp. 46–64, Springer, 2017.
Web page ⋅
Authors' PDF ⋅
Slides (PDF)
An Isabelle formalization of the expressiveness of deep learning (extended abstract)
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. In Hales, T. C., Kaliszyk, C., Schulz, S., Urban, J. (eds.) 2nd Conference on Artificial Intelligence and Theorem Proving (AITP 2017), pp. 22–23.
Abstract (PDF) ⋅
Slides (PDF)
Superposition for Higher-Order Logic
Alexander Bentkamp. Ph.D. thesis, Vrije Universiteit Amsterdam, 2021.
Ph.D. Thesis (PDF)
An Isabelle formalization of the expressiveness of deep learning
Alexander Bentkamp. M.Sc. thesis, Universität des Saarlandes, 2016.
M.Sc. Thesis (PDF)
Homologische Betrachtung des Alexanderpolynoms
Alexander Bentkamp. B.Sc. thesis, Georg-August-Universität Göttingen, 2013.
B.Sc. Thesis (PDF)
Embedding Path Order for Lambda-Free Higher-Order Terms
Alexander Bentkamp. Archive of Formal Proofs, 2018.
Formal proof development
Expressiveness of deep learning
Alexander Bentkamp. Archive of Formal Proofs, 2016.
Formal proof development
Latin Square
Alexander Bentkamp. Archive of Formal Proofs, 2016.
Formal proof development