Alexander Bentkamp

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.

a.bentkampvu.nl 0000-0002-7158-3595 +31 20 598 9544
Vrije Universiteit Amsterdam, Department of Computer Science, Room 12A71, De Boelelaan 1111, 1081 HV Amsterdam, Netherlands

News

I am a PhD now

On May 10, 2021, I successfully defended my PhD thesis.

Thesis (PDF)
Zipperposition Won Trophy

Zipperposition achieved first place in the higher-order division of the prover competition CASC 2020.

CASC website

Drafts:

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 materialSlides (PDF)

Publications:

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' PDFReport (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' PDFReport (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' PDFSupplementary 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 pageAuthors' PDFSupplementary 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 pageAuthors' PDFReport (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 pageAuthors' PDFReport (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 pageAuthors' 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 pageAuthors' PDFReport (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 pageAuthors' PDFSlides (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)

Theses:

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)

Formal proof developments:

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

Teaching: