I am a Ph.D. student of UT Vienna and wrote my master's thesis at the Theory and Logic Group. This page hosts an online version of it.
At the moment I'm contributing to the GAPT theorem proving framework hosted at github in the context of the CERES project.
If you are interested in hard problems for automated higher-order provers, you can find a collection here.
Feel free to contact me under 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
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]
Producing Skolem Expansion Trees with the CERES ω method: A Case Study, Workshop: Collegium Logicum Proof Theory: Herbrand's Theorem revisited, Vienna, Austria 2017 [slides]
Advanced Proof Viewing with PROOFTOOL, Workshop UITP 2014: User Interfaces for Theorem Provers, Vienna, Austria, 2014 [slides] [paper (as accepted for UITP)]
- 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