Cut-Elimination: Experiments with CERES. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (LPAR, 2004)

A Graph-Theoretic Approach to Steganography. - Stefan Hetzl; Petra Mutzel (Communications and Multimedia Security, 2005)

Proof Transformations and Structural Invariance. - Stefan Hetzl; Alexander Leitsch (Algebraic and Proof-theoretic Aspects of Non-classical Logics, 2006)

Proof Transformation by CERES. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (MKM, 2006)

Herbrand Sequent Extraction. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001; Bruno Woltzenlogel Paleo (AISC/MKM/Calculemus, 2008)

Transforming and Analyzing Proofs in the CERES-System. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001; Bruno Woltzenlogel Paleo (LPAR Workshops, 2008)

CERES: An analysis of Fürstenberg's proof of the infinity of primes. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (Theor. Comput. Sci., 2008)

A Clausal Approach to Proof Analysis in Second-Order Logic. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001; Bruno Woltzenlogel Paleo (LFCS, 2009)

Describing proofs by short tautologies. - Stefan Hetzl (Ann. Pure Appl. Log., 2009)

A Sequent Calculus with Implicit Term Representation. - Stefan Hetzl (CSL, 2010)

On the form of witness terms. - Stefan Hetzl (Arch. Math. Log., 2010)

CERES in higher-order logic. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001 (Ann. Pure Appl. Log., 2011)

On the non-confluence of cut-elimination. - Matthias Baaz; Stefan Hetzl (J. Symb. Log., 2011)

Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP). - Stefan Hetzl (AISC/MKM/Calculemus, 2012)

A Systematic Approach to Canonicity in the Classical Sequent Calculus. - Kaustuv Chaudhuri; Stefan Hetzl; Dale Miller 001 (CSL, 2012)

Herbrand-Confluence for Cut Elimination in Classical First Order Logic. - Stefan Hetzl; Lutz Straßburger (CSL, 2012)

Applying Tree Languages in Proof Theory. - Stefan Hetzl (LATA, 2012)

Towards Algorithmic Cut-Introduction. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001 (LPAR, 2012)

Bondy's Theorem. - Jeremy Avigad; Stefan Hetzl (Arch. Formal Proofs, 2012)

On the complexity of proof deskolemization. - Matthias Baaz; Stefan Hetzl; Daniel Weller 001 (J. Symb. Log., 2012)

The Computational Content of Arithmetical Proofs. - Stefan Hetzl (Notre Dame J. Formal Log., 2012)

Understanding Resolution Proofs through Herbrand's Theorem. - Stefan Hetzl; Tomer Libal; Martin Riener; Mikheil Rukhaia (TABLEAUX, 2013)

Herbrand-Confluence. - Stefan Hetzl; Lutz Straßburger (Log. Methods Comput. Sci., 2013)

Expansion Trees with Cut. - Stefan Hetzl; Daniel Weller 001 (CoRR, 2013)

Introducing Quantified Cuts in Logic with Equality. - Stefan Hetzl; Alexander Leitsch; Giselle Reis; Janos Tapolczai; Daniel Weller 001 (IJCAR, 2014)

The Cayley-Hamilton Theorem. - Stephan Adelsberger; Stefan Hetzl; Florian Pollak (Arch. Formal Proofs, 2014)

Algorithmic introduction of quantified cuts. - Stefan Hetzl; Alexander Leitsch; Giselle Reis; Daniel Weller 001 (Theor. Comput. Sci., 2014)

Tree Grammars for the Elimination of Non-prenex Cuts. - Stefan Hetzl; Sebastian Zivota (CSL, 2015)

Compressibility of Finite Languages by Grammars. - Sebastian Eberhard; Stefan Hetzl (DCFS, 2015)

Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars. - Bahareh Afshari; Stefan Hetzl; Graham Emil Leigh (TLCA, 2015)

Inductive theorem proving based on tree grammars. - Sebastian Eberhard; Stefan Hetzl (Ann. Pure Appl. Log., 2015)

System Description: GAPT 2.0. - Gabriel Ebner; Stefan Hetzl; Giselle Reis; Martin Riener; Simon Wolfsteiner; Sebastian Zivota (IJCAR, 2016)

On the Herbrand content of LK. - Bahareh Afshari; Stefan Hetzl; Graham E. Leigh (CL&C, 2016)

A multi-focused proof system isomorphic to expansion proofs. - Kaustuv Chaudhuri; Stefan Hetzl; Dale Miller 001 (J. Log. Comput., 2016)

Restricted notions of provability by induction. - Stefan Hetzl; Tin Lok Wong (CoRR, 2017)

Some observations on the logical foundations of inductive theorem proving. - Stefan Hetzl; Tin Lok Wong (Log. Methods Comput. Sci., 2017)

Preface. - Matthias Baaz; Agata Ciabattoni; Dov M. Gabbay; Stefan Hetzl; Daniel Weller 001 (J. Log. Comput., 2017)

Boolean unification with predicates. - Sebastian Eberhard; Stefan Hetzl; Daniel Weller 001 (J. Log. Comput., 2017)

Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars. - Sebastian Eberhard; Gabriel Ebner; Stefan Hetzl (ACM Trans. Comput. Log., 2017)

Complexity of Decision Problems on Totally Rigid Acyclic Tree Grammars. - Sebastian Eberhard; Gabriel Ebner; Stefan Hetzl (DLT, 2018)

On the compressibility of finite languages and formal proofs. - Sebastian Eberhard; Stefan Hetzl (Inf. Comput., 2018)

On the Generation of Quantified Lemmas. - Gabriel Ebner; Stefan Hetzl; Alexander Leitsch; Giselle Reis; Daniel Weller 001 (J. Autom. Reason., 2019)

Expansion trees with cut. - Federico Aschieri; Stefan Hetzl; Daniel Weller 001 (Math. Struct. Comput. Sci., 2019)

On the cover complexity of finite languages. - Stefan Hetzl; Simon Wolfsteiner (Theor. Comput. Sci., 2019)

Herbrand's theorem as higher order recursion. - Bahareh Afshari; Stefan Hetzl; Graham E. Leigh (Ann. Pure Appl. Log., 2020)

Clause Set Cycles and Induction. - Stefan Hetzl; Jannik Vierling (Log. Methods Comput. Sci., 2020)

Decidability of affine solution problems. - Stefan Hetzl; Sebastian Zivota (J. Log. Comput., 2020)

An Abstract Fixed-Point Theorem for Horn Formula Equations (Abstract). - Stefan Hetzl; Johannes Kloibhofer (SOQE@KR, 2021)

A Fixed-point Theorem for Horn Formula Equations. - Stefan Hetzl; Johannes Kloibhofer (HCVS@ETAPS, 2021)

Unprovability results for clause set cycles. - Stefan Hetzl; Jannik Vierling (Theor. Comput. Sci., 2022)

Induction and Skolemization in saturation theorem proving. - Stefan Hetzl; Jannik Vierling (Ann. Pure Appl. Log., 2023)

On the Completeness of Interpolation Algorithms. - Stefan Hetzl; Raheleh Jalali (LICS, 2024)

A Simplified Proof of the epsilon theorems. - Stefan Hetzl (Rev. Symb. Log., 2024)

Quantifier-free induction for lists. - Stefan Hetzl; Jannik Vierling (Arch. Math. Log., 2024)

Computing Witnesses Using the SCAN Algorithm. - Fabian Achammer; Stefan Hetzl; Renate A. Schmidt (CADE, 2025)

Computing Witnesses Using the SCAN Algorithm (Extended Preprint). - Fabian Achammer; Stefan Hetzl; Renate A. Schmidt (CoRR, 2025)