{"id":122,"date":"2022-09-03T12:19:24","date_gmt":"2022-09-03T12:19:24","guid":{"rendered":"https:\/\/www.anelalolic.com\/?page_id=122"},"modified":"2025-09-01T08:51:34","modified_gmt":"2025-09-01T08:51:34","slug":"pandaforest","status":"publish","type":"page","link":"https:\/\/www.anelalolic.com\/index.php\/research\/pandaforest\/","title":{"rendered":"PANDAFOREST"},"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<p><strong>P<\/strong>roof analysis <strong>and<\/strong> <strong>a<\/strong>utomated deduction <strong>fo<\/strong>r <strong>re<\/strong>cursive <strong>st<\/strong>ructures is a joint international project between Austria (funded by FWF, PI Anela Loli\u0107) and Czechia (funded by GA\u010cR, PI <a rel=\"noreferrer noopener\" href=\"https:\/\/www.cs.cas.cz\/dcerna\/index.html\" target=\"_blank\">David M. Cerna<\/a>) with a focus on computational proof theory and automated reasoning.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:33.33%\"><div class=\"wp-block-image\">\n<figure class=\"alignright size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"548\" height=\"645\" src=\"https:\/\/www.anelalolic.com\/wp-content\/uploads\/2022\/09\/pandaforest-1.png\" alt=\"\" class=\"wp-image-128\" style=\"width:261px;height:307px\" srcset=\"https:\/\/www.anelalolic.com\/wp-content\/uploads\/2022\/09\/pandaforest-1.png 548w, https:\/\/www.anelalolic.com\/wp-content\/uploads\/2022\/09\/pandaforest-1-255x300.png 255w, https:\/\/www.anelalolic.com\/wp-content\/uploads\/2022\/09\/pandaforest-1-380x447.png 380w\" sizes=\"auto, (max-width: 548px) 100vw, 548px\" \/><\/figure>\n<\/div><\/div>\n\n\n\n<div class=\"wp-block-column is-vertically-aligned-center is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:66.66%\">\n<ul class=\"wp-block-list\">\n<li>Name: <em>Proof analysis and automated deduction for recursive structures<\/em>.<\/li>\n\n\n\n<li>FWF project number: I 5848.<\/li>\n\n\n\n<li>Project timeline: Sept. 2022 &#8211; Nov 2025.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n\n\n\n<h2 class=\"wp-block-heading\">News<\/h2>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Our paper <em>Extracting Herbrand Systems from Refutation Schemata<\/em> (Alexander Leitsch and Anela Lolic) got accepted for publication at the Journal of Logic and Computation (to appear in 2025)!<\/li>\n\n\n\n<li>Our paper <em>Towards an Analysis of Proofs in Arithmetic<\/em> (Alexander Leitsch, Anela Lolic, and Stella Mahler) got accepted for publication at LSFA 2024!<\/li>\n\n\n\n<li>Stella Mahler will give a talk on <em>Proof Schemata and Primitive Recursive Arithmetic<\/em> at the Proof Society Meeting in Birmingham, September 1 &#8211; 13, 2024.<\/li>\n\n\n\n<li>Stella Mahler will give a talk on <em>Herbrand&#8217;s theorem for inductive proofs<\/em> at the Logic Colloquium 2024 in Gothenburg, Sweden, June 25.<\/li>\n\n\n\n<li>Our paper <a href=\"https:\/\/doi.org\/10.29007\/dwdf\" target=\"_blank\" rel=\"noreferrer noopener\">Herbrand\u2019s Theorem in Inductive Proofs<\/a> (Alexander Leitsch and Anela Lolic) got accepted for publication at LPAR 2024!<\/li>\n\n\n\n<li>Our paper <a href=\"https:\/\/doi.org\/10.29007\/4g2q\" target=\"_blank\" rel=\"noreferrer noopener\">On Proof Schemata and Primitive Recursive Arithmetic<\/a> (Alexander Leitsch, Anela Lolic, and Stella Mahler) got accepted for publication at LPAR 2024 Complementary Volume!<\/li>\n\n\n\n<li>Our preprint <a href=\"https:\/\/arxiv.org\/abs\/2402.13905\" target=\"_blank\" rel=\"noreferrer noopener\">Herbrand&#8217;s Theorem in Refutation Schemata<\/a>  (Alexander Leitsch and Anela Lolic)  is available on arXiv.<\/li>\n\n\n\n<li>Alexander Leitsch gave a talk on <em>First-Order Schemata and Herbrand&#8217;s theorem<\/em> at the TU Wien Computational Logic Seminar, May 22, 2024.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n\n\n\n<h2 class=\"wp-block-heading\"><strong>Description<\/strong><\/h2>\n\n\n\n<p>Mathematical induction is one of the essential concepts in the mathematician&#8217;s toolbox. Though, it has  proven itself difficult to handle formally.&nbsp; In essence, induction compresses an infinite argument into a finite statement. This process obfuscates information essential for computational proof transformation and automated reasoning. <strong>Herbrand\u2019s theorem<\/strong> covers the classical setting where this information can be finitely represented and used to analyze proofs and provide a formal foundation for automated theorem proving. While there are interpretations of Herbrand\u2019s theorem extending its scope to formal number theory, these results are at the expense of <strong>analyticity<\/strong>, the most desirable property of Herbrand\u2019s theorem.&nbsp; Given the rising importance of formal mathematics and inductive theorem proving to many areas of computer science, developing our understanding of the analyticity boundary is essential.<\/p>\n\n\n\n<p>In this project we tackle these issues using a relatively novel formulation of induction as sequences of proofs, referred to as <strong>proof schemata.<\/strong><em> <\/em>Proof schemata allow a recursive finite representation of many proof theoretically interesting objects as well as proof structures&nbsp;studied by the automated theorem proving community. Additionally, proof schemata provide the perfect framework to discuss <strong>proof analytic completeness<\/strong> of the method we plan to develop. This type of cyclic representation has been gaining traction the past few years and will in all likelihood play an integral role in automated theorem proving and proof theory in years to come. However, unlike other approaches to cyclic proof theory, we focus on the extraction of a finite representation of the <strong>Herbrand information<\/strong> contained in formal proofs. Development of a computational proof theoretic method for the extraction of Herbrand information for expressive inductive theories is our main objective. Furthermore, we hypothesize that developments in the proof theory of induction, using our chosen methodology (CERES style proof analysis), will lead to the development of more powerful inductive theorem provers.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\"><strong>Collaborators<\/strong><\/h2>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"https:\/\/www.dmg.tuwien.ac.at\/hetzl\/\" target=\"_blank\" rel=\"noreferrer noopener\">Stefan Hetzl<\/a> (TU Wien)<\/li>\n\n\n\n<li><a href=\"https:\/\/membres-lig.imag.fr\/peltier\/\" target=\"_blank\" rel=\"noreferrer noopener\">Nicolas Peltier<\/a> (CNRS, LIG)<\/li>\n\n\n\n<li><a href=\"https:\/\/www.mat.unb.br\/~dnantes\/index.html\" target=\"_blank\" rel=\"noreferrer noopener\">Daniele Nantes-Sobrinho<\/a> (UnB)<\/li>\n\n\n\n<li><a href=\"https:\/\/pure.royalholloway.ac.uk\/portal\/en\/persons\/reuben-rowe(70354339-7bc5-475d-b8d5-7fa95114d851).html\" target=\"_blank\" rel=\"noreferrer noopener\">Reuben Rowe<\/a> (Royal Holloway)<\/li>\n<\/ul>\n\n\n\n<h2 class=\"wp-block-heading\"><strong>Project Members<\/strong><\/h2>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Anela Loli\u0107 (PI, Austria)<\/li>\n\n\n\n<li><a href=\"https:\/\/www.cs.cas.cz\/dcerna\/\" target=\"_blank\" rel=\"noreferrer noopener\">David M. Cerna<\/a> (PI, Czechia)<\/li>\n\n\n\n<li><a href=\"https:\/\/www.logic.at\/staff\/leitsch\/\" target=\"_blank\" rel=\"noreferrer noopener\">Alexander Leitsch<\/a> (professor, Austria)<\/li>\n\n\n\n<li><a href=\"https:\/\/www.logic.at\/staff\/riener\/\" target=\"_blank\" rel=\"noreferrer noopener\">Martin Riener<\/a> (senior lecturer, Austria)<\/li>\n\n\n\n<li><a href=\"https:\/\/sites.google.com\/view\/rahelehjalali\/home?authuser=0\" target=\"_blank\" rel=\"noreferrer noopener\">Raheleh Jalali<\/a> (postdoc, Czechia)<\/li>\n\n\n\n<li>Stella Mahler (PhD student, Austria)<\/li>\n<\/ul>\n<\/div><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Proof analysis and automated deduction for recursive structures is a joint international project between Austria (funded by FWF, PI Anela Loli\u0107) and Czechia (funded by GA\u010cR, PI David M. Cerna) with a focus on computational proof theory and automated reasoning. News Description Mathematical induction is one of the essential concepts in the mathematician&#8217;s toolbox. Though, [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":23,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-122","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/pages\/122","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=122"}],"version-history":[{"count":29,"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/pages\/122\/revisions"}],"predecessor-version":[{"id":450,"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/pages\/122\/revisions\/450"}],"up":[{"embeddable":true,"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/pages\/23"}],"wp:attachment":[{"href":"https:\/\/www.anelalolic.com\/index.php\/wp-json\/wp\/v2\/media?parent=122"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}