Publications

2021

C. Eisenhofer, M. Riener: Automated Instantiation of Control Flow Tracing Exercises.. ThEdu 2021 [pdf]

G. Reger, M. Riener, M. Suda: Symmetry Avoidance in MACE-Style Finite Model Finding. FroCos 2019 [pdf]

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]

Instantiation for Theory Reasoning in Vampire, Vampire Workshop, Oxford, UK, 2018 [slides]
Instantiation for Theory Reasoning in Vampire, Automated Reasoning Workshop, Cambridge, UK, 2018 [abstract] [slides]
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]