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

• Skolemization and Equality, 2025-2029, funded by the FWF.
• Interpolation in Presence of Induction, 2024-2025, funded by an APART-MINT Fellowship of the Austrian Academy of Sciences.
• PANDAFOREST (Proof analysis and autom. deduction for recursive structures), 2022-2025, funded by the FWF.
• Globally Sound Proofs: New Frontiers of Analyticity, 2019, funded by a L’ORÉAL Austria PostDoc Fellowship of the Austrian Academy of Sciences.
• Automated Proof Analysis with CERES, 2018-2019, funded by a DOC Fellowship of the Austrian Academy of Sciences.

List of publications

• First-Order Schemata and Inductive Proof Analysis (with Alexander Leitsch and David M. Cerna). Springer 2026, ISBN 978-3-032-05740-2: 1-242.
• Epsilon Calculus Provides Shorter Cut-Free Proofs (with Matthias Baaz). Model Theory, Computer Science, and Graph Polynomials: Festschrift in Honor of Johann A. Makowsky. 65-75 (2025).
• Extracting Herbrand Systems from Refutation Schemata (with Alexander Leitsch). J. Log. Comput. 35(7) (2025).
• Efficient interpolation beyond cut-free proofs: Admissible cuts and optimized extraction (with Simon Corbard). ICTAC 2025: 185-201.
• An analytic representation of the semantics of first-order S5 (with Matthias Baaz and Mariami Gamsakhurdia). FroCoS 2025: 63-79.
• Towards an Analysis of Proofs in Arithmetic (with Alexander Leitsch and Stella Mahler). LSFA 2024: 98-111.
• On Translations of Epsilon Proofs to LK (with Matthias Baaz). LPAR 2024: 232-245.
• Herbrand’s Theorem in Inductive Proofs (with Alexander Leitsch). LPAR 2024: 295-310.
• On Proof Schemata and Primitive Recursive Arithmetic (with Alexander Leitsch and Stella Mahler). LPAR 2024 Complementary Volume, 117-130.
• Sequent Calculi for Choice Logics (with Michael Bernreiter, Jan Maly, and Stefan Woltran). J. Autom. Reason. 68(2): 8 (2024).
• Effective Skolemization (with Matthias Baaz). WoLLIC 2023: 69-82.
• 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.
• On the Unification of Term Schemata (with David M. Cerna and Alexander Leitsch). UNIF 2020: 6:1-6:6.
• 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.