Stefan Hetzl - Research

Publications

Journals

• A simplified proof of the epsilon theorems
  The Review of Symbolic Logic, 17(4), 1248-1263, 2024
  [ pdf, CUP ]
• Quantifier-free induction for lists (with J. Vierling)
  Archive for Mathematical Logic, 63, 813-835, 2024
  [ pdf, SpringerLink ]
• Induction and Skolemization in saturation theorem proving (with J. Vierling)
  Annals of Pure and Applied Logic, 174(1), 103167, 2023
  [ pdf, ScienceDirect ]
• Unprovability results for clause set cycles (with J. Vierling)
  Theoretical Computer Science, 935, 21-46, 2022
  [ pdf, ScienceDirect ]
• Clause Set Cycles and Induction (with J. Vierling)
  Logical Methods in Computer Science, 16(4), 2020
  [ episciences.org ]
• Herbrand's theorem as higher order recursion (with B. Afshari and G. E. Leigh)
  Annals of Pure and Applied Logic 171(6), 2020
  [ pdf, ScienceDirect ]
• Decidability of affine solution problems (with S. Zivota)
  Journal of Logic and Computation 30(3), 697-714, 2020
  [ pdf, Oxford Journals ]
• On the cover complexity of finite languages (with S. Wolfsteiner)
  Theoretical Computer Science 798, 109-125, 2019
  [ pdf, ScienceDirect ]
• Expansion trees with cut (with F. Aschieri and D. Weller)
  Mathematical Structures in Computer Science 29(8), 1009-1029, 2019
  [ pdf, Cambridge Core ]
• On the Generation of Quantified Lemmas (with G. Ebner, A. Leitsch, G. Reis, and D. Weller)
  Journal of Automated Reasoning, 63(1), 95-126, 2019
  [ pdf, SpringerLink ]
• On the compressibility of finite languages and formal proofs (with S. Eberhard)
  Information and Computation, 259, 191-213, 2018
  [ pdf, ScienceDirect ]
• Some observations on the logical foundations of inductive theorem proving (with T. L. Wong)
  Logical Methods in Computer Science, 13(4), 2018
  [ episciences.org ]
• Algorithmic compression of finite tree languages by rigid acyclic grammars (with S. Eberhard and G. Ebner)
  ACM Transactions on Computational Logic, 18(4), 2017
  [ pdf, ACM Digital Library ]
• Boolean unification with predicates (with S. Eberhard and D. Weller)
  Journal of Logic and Computation 27(1), 109-128, 2017
  [ pdf, Oxford Journals ]
• A multi-focused proof system isomorphic to expansion proofs (with K. Chaudhuri and D. Miller)
  Journal of Logic and Computation 26(2), 577-603, 2016
  [ pdf, Oxford Journals ]
• Inductive theorem proving based on tree grammars (with S. Eberhard)
  Annals of Pure and Applied Logic 166(6), 665-700, 2015
  [ pdf, ScienceDirect ]
• Algorithmic introduction of quantified cuts (with A. Leitsch, G. Reis and D. Weller)
  Theoretical Computer Science, 549, 1-16, 2014
  [ pdf, ScienceDirect ]
• Herbrand-Confluence (with L. Straßburger)
  Logical Methods in Computer Science 9(4), 2013
  [ episciences.org ]
• The Computational Content of Arithmetical Proofs
  Notre Dame Journal of Formal Logic 53(3), 289-296, 2012
  [ pdf, Project Euclid ]
• On the complexity of proof deskolemization (with M. Baaz and D. Weller)
  Journal of Symbolic Logic 77(2), 669-686, 2012
  [ pdf, Project Euclid ]
• CERES in Higher-Order Logic (with A. Leitsch and D. Weller)
  Annals of Pure and Applied Logic 162(12), 1001-1034, 2011
  [ pdf, ScienceDirect ]
• On the non-confluence of cut-elimination (with M. Baaz)
  Journal of Symbolic Logic 76(1), 313-340, 2011
  [ pdf, Project Euclid ]
• On the form of witness terms
  Archive for Mathematical Logic 49(5), 529-554, 2010
  [ pdf, SpringerLink ]
• Describing Proofs by Short Tautologies
  Annals of Pure and Applied Logic 159(1-2), 129-145, 2009
  [ pdf, ScienceDirect ]
• CERES: An Analysis of Fürstenberg's Proof of the Infinity of Primes (with M. Baaz, A. Leitsch, C. Richter and H. Spohr)
  Theoretical Computer Science 403(2-3), 160-175, 2008
  [ pdf, ScienceDirect ]

Conference Proceedings

• On the Completeness of Interpolation Algorithms (with R. Jalali)
  ACM/IEEE Symposium on Logic in Computer Science (LICS) 2024
  [ pdf, ACM Digital Library ]
• Complexity of decision problems on totally rigid acyclic tree grammars (with S. Eberhard and G. Ebner)
  Developments in Language Theory (DLT) 2018, M. Hoshi and S. Seki (eds.), Springer LNCS 11088
  [ pdf, SpringerLink ]
• Cover Complexity of Finite Languages (with S. Wolfsteiner)
  Descriptional Complexity of Formal Systems (DCFS) 2018, S. Konstantinidis and G. Pighizzini (eds.), Springer LNCS 10952
  [ pdf, SpringerLink ]
• Herbrand confluence for first-order proofs with Π₂-cuts (with B. Afshari and G. E. Leigh)
  Concepts of Proof in Mathematics, Philosophy, and Computer Science, D. Probst and P. Schuster (eds.), Ontos Mathematical Logic 6. De Gruyter. 2016.
  [ pdf, De Gruyter ]
• Herbrand's theorem revisited (with B. Afshari and G. E. Leigh)
  In: V. Bach and H. Fassbender, editors, Proceedings in Applied Mathematics and Mechanics, volume 16. Wiley-Vch. 2016.
  [ Wiley ]
• System Description: GAPT 2.0 (with G. Ebner, G. Reis, M. Riener, S. Wolfsteiner and S. Zivota)
  International Joint Conference in Automated Reasoning (IJCAR) 2016, N. Olivetti and A. Tiwari (eds.), Springer LNCS 9706
  [ pdf, SpringerLink ]
• 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 ]
• Compressibility of Finite Languages by Grammars (with S. Eberhard)
  Descriptional Complexity of Formal Systems (DCFS) 2015, J. Shallit and A. Okhotin (eds.), Springer LNCS 9118
  [ pdf, SpringerLink ]
• 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 ]
• Understanding Resolution Proofs through Herbrand's Theorem (with T. Libal, M. Riener, and M. Rukhaia)
  Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2013), D. Galmiche and D. Larchey-Wendling (eds.), Springer LNCS 8123
  [ pdf, SpringerLink ]
• A Systematic Approach to Canonicity in the Classical Sequent Calculus (with K. Chaudhuri and D. Miller)
  Computer Science Logic (CSL) 2012, P. Cégielski and A. Durand (eds.), Leibniz International Proceedings in Informatics (LIPIcs) 16
  [ DROPS ]
• Herbrand-Confluence for Cut Elimination in Classical First Order Logic (with L. Straßburger)
  Computer Science Logic (CSL) 2012, P. Cégielski and A. Durand (eds.), Leibniz International Proceedings in Informatics (LIPIcs) 16
  [ DROPS ]

• 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 ]

• Towards Algorithmic Cut-Introduction (with A. Leitsch and D. Weller)
  Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), N. Bjørner, A. Voronkov (eds.), Springer LNCS 7180
  [ pdf, SpringerLink ]
• Applying Tree Languages in Proof Theory
  Language and Automata Theory and Applications (LATA) 2012, A.-H. Dediu, C. Martín-Vide (eds.), Springer LNCS 7183
  [ pdf, SpringerLink ]
• A Sequent Calculus with Implicit Term Representation
  Computer Science Logic (CSL) 2010, A. Dawar, H. Veith (eds.), Springer LNCS 6247
  [ pdf, SpringerLink ]
• A Clausal Approach to Proof Analysis in Second-Order Logic (with A. Leitsch, D. Weller and B. Woltzenlogel Paleo)
  Logical Foundations of Computer Science, S. Artemov, A. Nerode (eds.), Springer LNCS 5407
  [ pdf, SpringerLink ]
• Herbrand Sequent Extraction (with A. Leitsch, D. Weller and B. Woltzenlogel Paleo)
  Intelligent Computer Mathematics, S. Autexier et al. (eds.), Springer LNAI 5144
  [ pdf, SpringerLink ]
• Proof Transformations and Structural Invariance (with A. Leitsch)
  Algebraic and Proof-theoretic Aspects of Non-classical Logics, S. Aguzzoli, A. Ciabattoni, B. Gerla, C. Manara and V. Marra (eds.), Springer LNCS 4460
  [ pdf, SpringerLink ]
• Proof Transformation by CERES (with M. Baaz, A. Leitsch, C. Richter and H. Spohr)
  5th International Conference on Mathematical Knowledge Management (MKM) 2006, Springer LNAI 4108
  [ pdf, SpringerLink ]
• A Graph-Theoretic Approach to Steganography (with P. Mutzel)
  9th IFIP Conference on Communications and Multimedia Security, CMS 2005, Springer LNCS 3677
  [ pdf, SpringerLink ]
• Cut-Elimination: Experiments with CERES, (with M. Baaz, A. Leitsch, C. Richter and H. Spohr)
  11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) 2004, Springer LNCS 3452
  [ pdf, SpringerLink ]

Formal Proofs

• Bondy's Theorem (with J. Avigad)
• The Cayley-Hamilton Theorem (with S. Adelsberger and F. Pollak)

Software

• GAPT – General Architecture for Proof Theory
• Ceres – Cut-Elimination by Resolution
• Steghide – Steganography

Theses

• A revised version of my PhD thesis is published as a book:
  Proof Profiles. Characteristic Clause Sets and Proof Transformations, VDM, Saarbrücken, 2008
  [ pdf ]
• PhD Thesis: Characteristic Clause Sets and Proof Transformations, Vienna University of Technology
  [ pdf ]
• Master's Thesis: Projection-Based Cut-Elimination and Normalization, Vienna University of Technology
  [ pdf ]

Preprints, Notes, Manuscripts, etc.

• Herbrand's Theorem as Higher Order Recursion (with B. Afshari and G. E. Leigh)
  Oberwolfach Preprint 2018-01
  [ MFO ]
• Why does induction require cut?
  [ pdf ]
• Undecidability Results for Simple Induction Proofs (with S. Eberhard)
  [ pdf ]
• Expansion Trees with Cut (with D. Weller)
  [ arXiv ]
• Proof Fragments, Cut-Elimination and Cut-Introduction
  [ pdf ]