I am a computer scientist working in logic, with a focus on proof theory. I am interested in structural proof theory, proof analysis and automated deduction.

Research projects

• PANDAFOREST (Proof analysis and autom. deduction for recursive structures), running, funded by the FWF.
• Globally Sound Proofs: New Frontiers of Analyticity, ended 2019, funded by a L’ORÉAL Austria PostDoc Fellowship of the Austrian Academy of Sciences.
• Automated Proof Analysis with CERES, ended 2019, funded by a DOC Fellowship of the Austrian Academy of Sciences.

List of publications

• Towards a proof theory for quantifier macros (with Matthias Baaz). Inf. Comput. 287: 104753 (2022)
• Sequent Calculi for Choice Logics (with Michael Bernreiter, Jan Maly, and Stefan Woltran). IJCAR 2022: 331-349
• Andrews Skolemization May Shorten Resolution Proofs Non-elementarily (with Matthias Baaz). LFCS 2022: 9-24
• Schematic Refutations of Formula Schemata (with David M. Cerna and Alexander Leitsch). J. Autom. Reason. 65(5): 599-645 (2021)
• Towards a proof theory for Henkin quantifiers (with Matthias Baaz). J. Log. Comput. 31(1): 40-66 (2021)
• An abstract form of the first epsilon theorem (with Matthias Baaz and Alexander Leitsch). J. Log. Comput. 30(8): 1447-1468 (2020)
• First-order interpolation derived from propositional interpolation (with Matthias Baaz). Theor. Comput. Sci. 837: 209-222 (2020)
• A Globally Sound Analytic Calculus for Henkin Quantifiers (with Matthias Baaz). LFCS 2020: 128-143
• Extraction of Expansion Trees (with Alexander Leitsch). J. Autom. Reason. 62(3): 393-430 (2019)
• Note on Globally Sound Analytic Calculi for Quantifier Macros (with Matthias Baaz). WoLLIC 2019: 486-497
• A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem (with Matthias Baaz and Alexander Leitsch). LFCS 2018: 55-71
• Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic (with Matthias Baaz). LPAR 2018: 95-110
• First-Order Interpolation of Non-classical Logics Derived from Propositional Interpolation (with Matthias Baaz). FroCoS 2017: 265-280