Stefan Hetzl - Teaching

On this page you can find some information about my teaching and supervision activities including links and material for download. For a complete listing of current courses, please consult my TISS page. I can offer student projects, master's theses, and Ph.D. theses on various topics connected to my research interests. If you want more specific information, do not hesitate to contact me.

Lectures

• Mathematisches Arbeiten für Informatik und Wirtschaftsinformatik (winter terms 2023/24, 2024/25), lecture notes (in German)
• Diskrete und geometrische Algorithmen (winter terms 2018/19, 2020/21, 2022/23), lecture notes (in German)
• Gödel's Incompleteness Theorems (summer terms 2018, 2020, 2022, 2024), lecture notes
• Automata and Formal Languages (winter terms 2015/16, 2016/17, summer terms 2019, 2021, 2023), lecture notes
• Theoretische Informatik (summer terms 2014-2019, 2021, 2024) lecture notes (in German)
• Automated Deduction (summer terms 2015, 2016)
• Higher-Order Logic (summer terms 2012, 2013), lecture notes
• Mathematical Logic 2 (summer terms 2009, 2011)
• Logical Foundations of Inductive Theorem Proving (2024), Eighteenth International Tbilisi Summer School in Logic and Language, slides
• Proof Theory of Induction (2018), International Summer School for Proof Theory in First-Order Logic, slides
• Automata and Formal Lanuage Theory (2013), Ninth International Tbilisi Summer School in Logic and Language, slides
• Complexity of Algorithms (2011), Seventh International Tbilisi Summer School in Logic and Language, slides

Ph.D. Theses

• Fabian Achammer: t.b.d., in progress
• Jannik Vierling: The limits of automated inductive theorem provers, 2024
  [ pdf, UBTUW ]
• Sebastian Zivota: On formula equations and invariant generation, 2021
  [ pdf, UBTUW ]
• Gabriel Ebner: Inductive theorem proving using tree grammars, 2021
  [ pdf, UBTUW ]
• Simon Wolfsteiner: Grammatical Complexity of Finite Languages, 2020
  [ pdf, UBTUW ]

Master's Theses

• Johannes Weiser: Subsystems of Open Induction, 2025
  [ pdf ]
• Fabian Achammer: Decidability of Diophantine equations in a theory adjacent to IOpen, 2023
  [ pdf, UBTUW ]
• Johannes Kloibhofer: A fixed-point theorem for Horn formula equations, 2020
  [ pdf, UBTUW ]
• Jannik Vierling: Cyclic superposition and induction, 2018
  [ pdf, UBTUW ]
• Hugo Moeneclaey: Expansion proofs for arithmetic, Stage M2, Master Parisien de Recherche en Informatique (MPRI), 2017
  [ pdf ]
• Andreas Humenberger: Abstract proof structures, 2016
  [ pdf, UBTUW ]
• Gabriel Ebner: Finding loop invariants using tree grammars, 2015
  [ pdf, UBTUW ]
• Bernhard Mallinger: Interpolation in first-order logic with equality, 2014
  [ pdf, UBTUW ]
• Sebastian Zivota: Cuts without quantifier alternations and their effect on expansion trees, 2014
  [ pdf, UBTUW ]

Bachelor's Theses

• Manuel Schweigler: Proof Systems for Regular Expressions, 2025
  [ pdf ]
• Tobias Leichtfried: A formal proof of the equivalence between pushdown automata and context-free grammars, 2025
  [ pdf ]
• Fabian Wöhrer: Reversible Automata: Characterizations and Construction, 2024
  [ pdf ]
• Florian Grünstäudl: The Beth Definability Theorem and the Complexity of Explicit Definitions, 2024
  [ pdf ]
• Clara Pichler: The Tutte Polynomial, 2024
  [ pdf ]
• Johannes Weiser: Varieties of rational languages and finite monoids, 2023
  [ pdf ]
• Leopold Fajtak: Programmextraktion mittels Gödels Dialectica Interpretation, 2022
  [ pdf ]
• Fabian Achammer: Eine Variante des DLS-Algorithmus zum Lösen von Formelgleichungen, 2020
  [ pdf ]
• Martin Gius: Die Unentscheidbarkeit der k-Beweisbarkeit, 2019
  [ pdf ]
• Markus Rinke: Die Kosten eines Zyklus sind ein Quadrat, 2019
  [ pdf ]

Internships

• Parham Shadman: The regular cover problem, 2024
• Andreas Halkjær From: Spin - Superposition with Structural Induction, 2019, internship report
• Jannik Vierling: AIP's induction axioms, 2017
• Alexander Birch Jensen: gaptic - Tactic-language for proof formalization, 2016, internship report
• Janos Tapolczai: Cut Introduction - Cut-Formulas with Multiple Universal Quantifiers, 2014

Seminar papers

• Raphael Gruber: Boolean Equations, winter term 2024/25
• Johanne Müller Vistisen: NP-Completeness of the Smallest 1-Level Grammar Problem, summer term 2024
• Johannes Weiser: Complexity Bounds for Cut Elimination, summer term 2024
• Johannes Weiser: Star height of rational languages, summer term 2023
• Seminar on J. Krajíček: Proof Complexity, Cambridge University Press, 2019, summer term 2022:
  • Fabian Achammer: Untere Beweisschranken durch effiziente Interpolation
  • Fabian Regen: Upper bounds on Frege proofs of the pigeonhole principle via the Paris-Wilkie translation

• Seminar on R. Kaye: Models of Peano Arithmetic, Oxford University Press, 1991, winter term 2020
  • Leo Brauner: Ordnungstypen von Nichtstandardmodellen der Peano-Arithmetik
  • Stefan Schrott: Gaifmans Splitting Theorem
  • Leopold Fajtak: Primmodelle, Typen und Enderweiterungen in PA
  • Paul Hotzy: Untertheorien von PA
  • Johannes Kloibhofer: Saturiertheit

• Seminar on H. Straubing: Finite Automata, Formal Logic, and Circuit Complexity, Springer, 1994, winter term 2019
  • Stefan Schrott: Charakterisierung regulärer Sprachen und regulärer numerischer Prädikate durch logische Formeln
  • Paul Hotzy: Modelltheoretische Spiele
  • Tomáš Nagy: Endliche Halbgruppen
  • Leo Brauner: Charakterisierungen der Sprachen in FO[<], FO[+1] und FO[Reg] mittels syntaktischem Monoid und Homomorphismus
  • Lucas Unterberger: Modulare Quantoren
  • Alexandra Bergmayr: Schaltkreiskomplexität
  • Charlotte Jergitsch: Reguläre Sprachen und Schaltkreiskomplexität

• Markus Rinke: Der Gentzensche Hauptsatz, summer term 2019
• Seminar on N. Immerman: Descriptive Complexity, Springer, 1999, summer term 2018
• Johannes Kloibhofer: First-order Reduktionen
• Markus Peschl: Erfassung deterministischer Polynomialzeit mittels kleinsten Fixpunktoperatoren
• Martin Gius: Ehrenfeucht-Fraïssé Spiele
• Alexander Kövesdi: Prädikatenlogik zweiter Stufe und der Satz von Fagin