Photo of me

I am a researcher at The University of Manchester working on the Vampire automated theorem prover. In my previous position in the Veridis team at INRIA Nancy I was working on TLAPM, an interactive theorem prover for the temporal logic TLA+. During my PhD at the Theory and Logic Group at TU Wien, I was working on CERESω, a cut-elimination method for higher-order proofs using automated theorem provers. During this time, I also contributed to the GAPT framework for proof theory. On this page you can find the online versions of my thesis and the papers I co-authored.

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

Feel free to contact me under martin [at] derivation [dot] org or riener [at] logic [dot] at.

Publications

2018

2016

2014

2013

2012

Thesis

Talks

Posters