Algorithmic Structuring and Compression of Proofs

In this project we develop algorithms and software for structuring and compressing formal proofs. These algorithms are based on proof-theoretic results, in particular a recently discovered connection between proof theory and formal language theory. Please see the project description (or the poster) for more detailed information. This work is funded by the Austrian Science Fund (FWF) as project number P25160.

Software

Our implementation is based on the GAPT project and is currently carried out in GAPT's codebase.

Publications

• Tree Grammars for the Elimination of Non-prenex Cuts (with S. Zivota)
  Computer Science Logic (CSL) 2015, S. Kreutzer (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 41
  [ DROPS ]
• Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars (with B. Afshari and G. E. Leigh)
  Typed Lambda Calculi and Applications (TLCA) 2015, T. Altenkirch (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 38
  [ DROPS ]
• Algorithmic introduction of quantified cuts (with A. Leitsch, G. Reis and D. Weller)
  Theoretical Computer Science, 549, 1-16, 2014
  [ pdf, ScienceDirect ]
• Introducing Quantified Cuts in Logic with Equality (with A. Leitsch, G. Reis, J. Tapolczai and D. Weller)
  International Joint Conference in Automated Reasoning (IJCAR) 2014, S. Demri, D. Kapur and C. Weidenbach (eds.), Springer LNCS 8562
  [ pdf, SpringerLink ]

• S. Hetzl. Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP)
  Conferences on Intelligent Computer Mathematics (CICM) 2012, J. Jeuring et al. (eds.), Springer LNAI 7362
  [ pdf, SpringerLink ]

  Poster accompanying the project presentation
  [ pdf ]

• S. Hetzl, A. Leitsch and D. Weller. Towards Algorithmic Cut-Introduction
  Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), N. Bjørner, A. Voronkov (eds.), Springer LNCS 7180
  [ pdf, SpringerLink ]

---

Last Change: 2016-04-13, Stefan Hetzl