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.
- G. Ebner, S. Hetzl, G. Reis, M. Riener, S. Wolfsteiner, S. Zivota: System Description: GAPT 2.0. IJCAR 2016: 293-301 [pdf]
- T. Libal, M. Riener, M. Rukhaia: Advanced Proof Viewing in PROOFTOOL. UITP 2014: 35-47 [pdf]
- S. Hetzl, T. Libal, M. Riener, M. Rukhaia: Understanding Resolution Proofs through Herbrand's Theorem. TABLEAUX 2013: 157-171 [pdf]
- C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, B. Woltzenlogel Paleo: PROOFTOOL: a GUI for the GAPT Framework. EPTCS 118, Proceedings 10th International Workshop On User Interfaces for Theorem Provers, 2012: 1-14 [pdf]
- C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, B. Woltzenlogel Paleo. System Feature Description: Importing Refutations into the GAPT Framework. Proceedings of the 2nd International Workshop on Proof Exchange for Theorem Proving, 2012: 51-57 [pdf]
- PhD thesis "Applications of Higher-Order Cut-Elimination"
- Master thesis "Integrating Theories into Inference Systems"
Producing Skolem Expansion Trees with the CERES ω method: A Case Study, Workshop: Collegium Logicum Proof Theory: Herbrand's Theorem revisited, Vienna, Austria 2017 [slides]
- Understanding Resolution Proofs through Herbrand's Theorem, TbiLLC 2013: Tenth International Tbilisi Symposium on Language, Logic and Computation, Gudauri, Georgia, 2013 [slides]
- System Feature Description: Importing Refutations into the GAPT Framework, Proof Exchange for Theorem Proving - Second International Workshop (PxTP), Manchester, United Kingdom, 2012 [slides]
- Poster of the presentation of the thesis