My current focus lies on improving the support for the theory of arrays in the Vampire prover. I am particularly interested in proving conjectures of the form "There exists an array with the following properties: ...".

Previously I was working on TLAPM, an interactive theorem prover for the temporal logic TLA+.

A main motivation for my current activities comes from my work on CERESĪ‰, a cut-elimination method for higher-order proofs using automated theorem provers. For my PhD thesis, I used the method to extract function definitions from proofs in higher-order logic. All experiments were done using the GAPT framework for proof theory to which I am still contributing from time to time.

If you are interested in hard problems for automated higher-order provers, you can find a collection here.

about me · research · publications · teaching · outreach · software · contact · home