{"id":23,"date":"2022-09-02T08:27:17","date_gmt":"2022-09-02T08:27:17","guid":{"rendered":"https:\/\/www.anelalolic.com\/?page_id=23"},"modified":"2026-03-30T13:11:51","modified_gmt":"2026-03-30T13:11:51","slug":"research","status":"publish","type":"page","link":"https:\/\/www.anelalolic.com\/index.php\/research\/","title":{"rendered":"Research"},"content":{"rendered":"\n<div class=\"wp-block-group has-background\" style=\"background-color:#ffffffb3\"><div class=\"wp-block-group__inner-container is-layout-flow wp-block-group-is-layout-flow\">\n<h2 class=\"wp-block-heading\">Research projects<\/h2>\n\n\n\n<ul class=\"wp-block-list\">\n<li><em>Skolemization and Equality<\/em>, 2025-2029, funded by the FWF.<\/li>\n\n\n\n<li><em>Interpolation in Presence of Induction<\/em>, 2024-2025, funded by an <a href=\"https:\/\/stipendien.oeaw.ac.at\/en\/fellowships\/apart-mint\" target=\"_blank\" rel=\"noreferrer noopener\">APART-MINT Fellowship<\/a> of the Austrian Academy of Sciences.<\/li>\n\n\n\n<li><a href=\"https:\/\/www.anelalolic.com\/index.php\/research\/pandaforest\/\" target=\"_blank\" rel=\"noreferrer noopener\">PANDAFOREST <\/a>(<em>Proof analysis and autom. deduction for recursive structures<\/em>), 2022-2025, funded by the FWF.<\/li>\n\n\n\n<li><em>Globally Sound Proofs: New Frontiers of Analyticity<\/em>, 2019, funded by a <a href=\"https:\/\/stipendien.oeaw.ac.at\/en\/fellowships\/loreal-austria\" target=\"_blank\" rel=\"noreferrer noopener\">L\u2019OR\u00c9AL Austria PostDoc Fellowship<\/a> of the Austrian Academy of Sciences.<\/li>\n\n\n\n<li><em>Automated Proof Analysis with CERES<\/em>, 2018-2019, funded by a <a href=\"https:\/\/stipendien.oeaw.ac.at\/en\/stipendien\/doc\" target=\"_blank\" rel=\"noreferrer noopener\">DOC Fellowship<\/a> of the Austrian Academy of Sciences.<\/li>\n<\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">List of publications<\/h2>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"https:\/\/link.springer.com\/book\/10.1007\/978-3-032-05741-9\" target=\"_blank\" rel=\"noreferrer noopener\">First-Order Schemata and Inductive Proof Analysis<\/a> (with Alexander Leitsch and David M. Cerna). Springer 2026, ISBN 978-3-032-05740-2: 1-242.<\/li>\n\n\n\n<li><a href=\"https:\/\/doi.org\/10.1007\/978-3-031-86319-6_7\" target=\"_blank\" rel=\"noreferrer noopener\">Epsilon Calculus Provides Shorter Cut-Free Proofs<\/a> (with Matthias Baaz). Model Theory, Computer Science, and Graph Polynomials: Festschrift in Honor of Johann A. Makowsky. 65-75 (2025).<\/li>\n\n\n\n<li><a href=\"https:\/\/doi.org\/10.1093\/logcom\/exaf010\" target=\"_blank\" rel=\"noreferrer noopener\">Extracting Herbrand Systems from Refutation Schemata<\/a> (with Alexander Leitsch). J. Log. Comput. 35(7) (2025).<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-032-11176-0_12\" target=\"_blank\" rel=\"noreferrer noopener\">Efficient interpolation beyond cut-free proofs: Admissible cuts and optimized extraction<\/a> (with Simon Corbard). ICTAC 2025: 185-201.<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-032-04167-8_4\" target=\"_blank\" rel=\"noreferrer noopener\">An analytic representation of the semantics of first-order S5<\/a> (with Matthias Baaz and Mariami Gamsakhurdia). FroCoS 2025: 63-79.<\/li>\n\n\n\n<li><a href=\"https:\/\/arxiv.org\/abs\/2506.05837v1\" target=\"_blank\" rel=\"noreferrer noopener\">Towards an Analysis of Proofs in Arithmetic<\/a> (with Alexander Leitsch and Stella Mahler). LSFA 2024: 98-111.<\/li>\n\n\n\n<li><a href=\"https:\/\/doi.org\/10.29007\/9pts\" target=\"_blank\" rel=\"noreferrer noopener\">On Translations of Epsilon Proofs to LK<\/a> (with Matthias Baaz). LPAR 2024: 232-245.<\/li>\n\n\n\n<li><a href=\"https:\/\/doi.org\/10.29007\/dwdf\" target=\"_blank\" rel=\"noreferrer noopener\">Herbrand&#8217;s Theorem in Inductive Proofs<\/a> (with Alexander Leitsch). LPAR 2024: 295-310.<\/li>\n\n\n\n<li><a href=\"https:\/\/doi.org\/10.29007\/4g2q\" target=\"_blank\" rel=\"noreferrer noopener\">On Proof Schemata and Primitive Recursive Arithmetic<\/a> (with Alexander Leitsch and Stella Mahler). LPAR 2024 Complementary Volume, 117-130.<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09695-5\">Sequent Calculi for Choice Logics<\/a> (with Michael Bernreiter, Jan Maly, and Stefan Woltran). <a href=\"https:\/\/dblp.uni-trier.de\/db\/journals\/jar\/jar68.html#BernreiterLMW24\">J. Autom. Reason. 68(2)<\/a>: 8 (2024).<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-39784-4_5\">Effective Skolemization<\/a> (with Matthias Baaz). WoLLIC 2023: 69-82.<\/li>\n\n\n\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540121000687?via%3Dihub\" target=\"_blank\" rel=\"noreferrer noopener\">Towards a proof theory for quantifier macros<\/a> (with Matthias Baaz). Inf. Comput. 287: 104753 (2022).<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-10769-6_20\" target=\"_blank\" rel=\"noreferrer noopener\">Sequent Calculi for Choice Logics<\/a> (with Michael Bernreiter, Jan Maly, and Stefan Woltran). <a href=\"https:\/\/dblp.uni-trier.de\/db\/conf\/cade\/ijcar2022.html#BernreiterLMW22\">IJCAR 2022<\/a>: 331-349.<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-93100-1_2\" target=\"_blank\" rel=\"noreferrer noopener\">Andrews Skolemization May Shorten Resolution Proofs Non-elementarily<\/a> (with Matthias Baaz). LFCS 2022: 9-24.<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09583-8\" target=\"_blank\" rel=\"noreferrer noopener\">Schematic Refutations of Formula Schemata<\/a> (with David M. Cerna and Alexander Leitsch). J. Autom. Reason. 65(5): 599-645 (2021).<\/li>\n\n\n\n<li><a href=\"https:\/\/academic.oup.com\/logcom\/article-abstract\/31\/1\/40\/6042512?redirectedFrom=fulltext&amp;login=false\" target=\"_blank\" rel=\"noreferrer noopener\">Towards a proof theory for Henkin quantifiers<\/a> (with Matthias Baaz). J. Log. Comput. 31(1): 40-66 (2021).<\/li>\n\n\n\n<li><a href=\"https:\/\/academic.oup.com\/logcom\/article-abstract\/30\/8\/1447\/5911457?redirectedFrom=fulltext&amp;login=false\" target=\"_blank\" rel=\"noreferrer noopener\">An abstract form of the first epsilon theorem<\/a> (with Matthias Baaz and Alexander Leitsch). J. Log. Comput. 30(8): 1447-1468 (2020).<\/li>\n\n\n\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/abs\/pii\/S0304397520304266?via%3Dihub\">First-<\/a><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/abs\/pii\/S0304397520304266?via%3Dihub\" target=\"_blank\" rel=\"noreferrer noopener\">order i<\/a><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/abs\/pii\/S0304397520304266?via%3Dihub\">nterpolation derived from propositional interpolation<\/a> (with Matthias Baaz). Theor. Comput. Sci. 837: 209-222 (2020).<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-36755-8_9\" target=\"_blank\" rel=\"noreferrer noopener\">A Globally Sound Analytic Calculus for Henkin Quantifier<\/a>s (with Matthias Baaz). LFCS 2020: 128-143.<\/li>\n\n\n\n<li><a href=\"http:\/\/www3.risc.jku.at\/publications\/download\/risc_6129\/proceedings-UNIF2020.pdf#page=33\">On the Unification of Term Schemata<\/a> (with David M. Cerna and Alexander Leitsch). UNIF 2020: 6:1-6:6.<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10817-018-9453-9\" target=\"_blank\" rel=\"noreferrer noopener\">Extraction of Expansion Trees<\/a> (with Alexander Leitsch). J. Autom. Reason. 62(3): 393-430 (2019).<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-662-59533-6_29\" target=\"_blank\" rel=\"noreferrer noopener\">Note on Globally Sound Analytic Calculi for Quantifier Macros<\/a> (with Matthias Baaz). WoLLIC 2019: 486-497.<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-319-72056-2_4\" data-type=\"URL\" data-id=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-319-72056-2_4\" target=\"_blank\" rel=\"noreferrer noopener\">A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem<\/a> (with Matthias Baaz and Alexander Leitsch). LFCS 2018: 55-71.<\/li>\n\n\n\n<li><a href=\"https:\/\/easychair.org\/publications\/paper\/v6Sp\" target=\"_blank\" rel=\"noreferrer noopener\">Lyndon Interpolation holds for the Prenex \u2283 Prenex Fragment of G\u00f6del Logic<\/a> (with Matthias Baaz). LPAR 2018: 95-110.<\/li>\n\n\n\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-319-66167-4_15\" target=\"_blank\" rel=\"noreferrer noopener\">First-Order Interpolation of Non-classical Logics Derived from Propositional Interpolation<\/a> (with Matthias Baaz). FroCoS 2017: 265-280.<\/li>\n<\/ul>\n<\/div><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Research projects List of publications<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":2,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-23","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/pages\/23","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/comments?post=23"}],"version-history":[{"count":42,"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/pages\/23\/revisions"}],"predecessor-version":[{"id":492,"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/pages\/23\/revisions\/492"}],"wp:attachment":[{"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/media?parent=23"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}