Stefan Hetzl  Research
Publications
Journals

A simplified proof of the epsilon theorems
The Review of Symbolic Logic, published online, 2023
[ pdf, CUP ] 
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, 2146, 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), 697714, 2020
[ pdf, Oxford Journals ] 
On the cover complexity of finite languages (with S. Wolfsteiner)
Theoretical Computer Science 798, 109125, 2019
[ pdf, ScienceDirect ] 
Expansion trees with cut (with F. Aschieri and D. Weller)
Mathematical Structures in Computer Science 29(8), 10091029, 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), 95126, 2019
[ pdf, SpringerLink ] 
On the compressibility of finite languages and formal proofs (with S. Eberhard)
Information and Computation, 259, 191213, 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), 109128, 2017
[ pdf, Oxford Journals ] 
A multifocused proof system isomorphic to expansion proofs (with K. Chaudhuri and D. Miller)
Journal of Logic and Computation 26(2), 577603, 2016
[ pdf, Oxford Journals ] 
Inductive theorem proving based on tree grammars (with S. Eberhard)
Annals of Pure and Applied Logic 166(6), 665700, 2015
[ pdf, ScienceDirect ] 
Algorithmic introduction of quantified cuts (with A. Leitsch, G. Reis and D. Weller)
Theoretical Computer Science, 549, 116, 2014
[ pdf, ScienceDirect ] 
HerbrandConfluence (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), 289296, 2012
[ pdf, Project Euclid ] 
On the complexity of proof deskolemization (with M. Baaz and D. Weller)
Journal of Symbolic Logic 77(2), 669686, 2012
[ pdf, Project Euclid ] 
CERES in HigherOrder Logic (with A. Leitsch and D. Weller)
Annals of Pure and Applied Logic 162(12), 10011034, 2011
[ pdf, ScienceDirect ] 
On the nonconfluence of cutelimination (with M. Baaz)
Journal of Symbolic Logic 76(1), 313340, 2011
[ pdf, Project Euclid ] 
On the form of witness terms
Archive for Mathematical Logic 49(5), 529554, 2010
[ pdf, SpringerLink ] 
Describing Proofs by Short Tautologies
Annals of Pure and Applied Logic 159(12), 129145, 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(23), 160175, 2008
[ pdf, ScienceDirect ]
Conference Proceedings

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 firstorder proofs with Π_{2}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. WileyVch. 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 Nonprenex 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 ContextFree 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. LarcheyWendling (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 ] 
HerbrandConfluence 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 CutIntroduction (with A. Leitsch and D. Weller)
Logic for Programming, Artificial Intelligence and Reasoning (LPAR18), 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ínVide (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 SecondOrder 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 Prooftheoretic Aspects of Nonclassical 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 GraphTheoretic Approach to Steganography (with P. Mutzel)
9th IFIP Conference on Communications and Multimedia Security, CMS 2005, Springer LNCS 3677
[ pdf, SpringerLink ] 
CutElimination: 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 CayleyHamilton Theorem (with S. Adelsberger and F. Pollak)
Software
 GAPT – General Architecture for Proof Theory
 Ceres – CutElimination 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: ProjectionBased CutElimination 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 201801
[ 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, CutElimination and CutIntroduction
[ pdf ]
Last Change: 20240612, Stefan Hetzl