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
- Interpolation in Presence of Induction, to start in November 2024, funded by an APART-MINT Fellowship of the Austrian Academy of Sciences.
- 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
- 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