TU Wien Informatics

Overview Professors Scientific Staff Administrative Staff Student Staff External Lecturers By Responsibilities By Committee By Name
Related
Guest Professors Honoraries Alumni (LinkedIn) #5qw

Stefan Hetzl

Associate Prof. Dipl.-Ing. Dr.techn. / BSc

Research Areas

  • Interactive theorem proving, Automated theorem proving, Proof Theory, Theory of formal Languages
Stefan Hetzl

About

Computational Logic, Proof Theory, Theory of Formal Languages, Automated theorem proving, Interactive theorem proving

Role

Contact

2024W

2025S

 

2019

  • Expansion trees with cut / Aschieri, F., Hetzl, S., & Weller, D. (2019). Expansion trees with cut. Mathematical Structures in Computer Science, 29(8), 1009–1029. https://doi.org/10.1017/s0960129519000069

2017

  • Preface / Baaz, M., Ciabattoni, A., Gabbay, D. M., Hetzl, S., & Weller, D. (2017). Preface. Journal of Logic and Computation, 27(2), 415–415. https://doi.org/10.1093/logcom/exu076

2016

  • System Description: GAPT 2.0 / Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S. P., & Zivota, S. (2016). System Description: GAPT 2.0. In Automated Reasoning (pp. 293–301). Springer. https://doi.org/10.1007/978-3-319-40229-1_20
    Project: ASCP (2013–2016)

2014

2013

  • Herbrand-Confluence / Hetzl, S., & Strassburger, L. (2013). Herbrand-Confluence. Logical Methods in Computer Science, 9(4). https://doi.org/10.2168/LMCS-9(4:24)2013

2012

  • Towards Algorithmic Cut-Introduction / Leitsch, A., Hetzl, S., & Weller, D. (2012). Towards Algorithmic Cut-Introduction. In N. Bjørner & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (pp. 228–242). Springer LNCS. https://doi.org/10.1007/978-3-642-28717-6_19

2011

  • On the non-confluence of cut-elimination / Baaz, M., & Hetzl, S. (2011). On the non-confluence of cut-elimination. Journal of Symbolic Logic, 76(1), 313–340. https://doi.org/10.2178/jsl/1294171002
  • Ceres in higher-order logic / Hetzl, S., Leitsch, A., & Weller, D. (2011). Ceres in higher-order logic. Annals of Pure and Applied Logic, 162(12), 1001–1034. https://doi.org/10.1016/j.apal.2011.06.005

2010

  • On the complexity of proof deskolemization / Baaz, M., Hetzl, S., & Weller, D. (2010). On the complexity of proof deskolemization. Collegium Locicum 2010: Proofs and Structures, Paris, EU. http://hdl.handle.net/20.500.12708/85099
  • CERES in higher-order-logic / Hetzl, S., Leitsch, A., & Weller, D. (2010). CERES in higher-order-logic. Workshop on Classical Logic and Computation (CL&C’10), Brünn, EU. http://hdl.handle.net/20.500.12708/85096

2009

  • A Clausal Approach to Proof Analysis in Second-Order Logic / Hetzl, S., Leitsch, A., Weller, D., & Woltzenlogel-Paleo, B. (2009). A Clausal Approach to Proof Analysis in Second-Order Logic. In A. Nerode & S. Artemov (Eds.), LFCS 2009: Logical Foundations of Computer Science (pp. 214–229). Springer, LNCS. https://doi.org/10.1007/978-3-540-92687-0_15

2008

  • CERES: An analysis of Fürstenberg's proof of the infinity of primes / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2008). CERES: An analysis of Fürstenberg’s proof of the infinity of primes. Theoretical Computer Science, 403(2–3), 160–175. https://doi.org/10.1016/j.tcs.2008.02.043
  • Cut-elimination / Baaz, M., & Hetzl, S. (2008). Cut-elimination. Third Vienna Tbilisi Summer School in Logic and Language, Tbilisi, Georgia, Non-EU. http://hdl.handle.net/20.500.12708/118581
  • Herbrand Sequent Extraction / Leitsch, A., Hetzl, S., Weller, D., & Woltzenlogel-Paleo, B. (2008). Herbrand Sequent Extraction. In S. Autexier (Ed.), AISC/Calculemus/MKM 2008 (pp. 462–477). Springer. http://hdl.handle.net/20.500.12708/52369
  • Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions / Leitsch, A., Hetzl, S., Weller, D., & Woltzenlogel-Paleo, B. (2008). Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions. In G. Sutcliffe, S. Colton, & S. Schulz (Eds.), Proceedings of the CICIM Workshops on ESARM-08 (pp. 23–41). CEUR-WS.org. http://hdl.handle.net/20.500.12708/52368
  • Transforming and Analyzing Proofs in the CERES-system / Leitsch, A., Hetzl, S., Weller, D., & Woltzenlogel-Paleo, B. (2008). Transforming and Analyzing Proofs in the CERES-system. In P. Rudnicki & G. Sutcliffe (Eds.), Proceedings of the LPAR 2008 Workshops (pp. 77–91). CEUR-WS.org. http://hdl.handle.net/20.500.12708/52364

2007

  • Proof Transformations and Structural Invariance / Leitsch, A., & Hetzl, S. (2007). Proof Transformations and Structural Invariance. In S. Aguzzoli (Ed.), LNAI 4460: Algebraic and Proof-theoretic Aspects (pp. 201–230). Springer, LNAI 4460. http://hdl.handle.net/20.500.12708/25413
  • Characteristic clause sets and proof transformations / Hetzl, S. (2007). Characteristic clause sets and proof transformations [Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/183195

2006

  • A Similarity Criterion for Proofs (abstract) / Hetzl, S. (2006). A Similarity Criterion for Proofs (abstract). In A. Beckmann, U. Berger, B. Löwe, & J. V. Tucker (Eds.), Logical Approaches to Computational Barriers (p. 295). University of Wales Swansea Report Series. http://hdl.handle.net/20.500.12708/51677
  • System Description: The Cut-Elimination System CERES / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2006). System Description: The Cut-Elimination System CERES. In G. Sutcliffe, R. Schmidt, & S. Schulz (Eds.), ESCoR 2006 Empirically Successful Computerized Reasoning (p. 9). CEUR Workshop Proceedings. http://hdl.handle.net/20.500.12708/176627
  • Proof transformation by CERES / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2006). Proof transformation by CERES. Lecture Notes in Computer Science, 82–93. https://doi.org/10.1007/11812289_8
  • Comparing Mathematical Proofs / Hetzl, S. (2006). Comparing Mathematical Proofs. Studia Logica International Conference; Towards Mathematical Philosophy; Trends in Logic IV, Torun, Poland, EU. http://hdl.handle.net/20.500.12708/84554
  • Proof Transformation by CERES / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2006). Proof Transformation by CERES. In J. M. Borwein & W. Farmer (Eds.), MKM 2006 (pp. 82–93). Springer. http://hdl.handle.net/20.500.12708/51679

2005

  • A Graph-Theoretic Approach to Steganography / Hetzl, S., & Mutzel, P. (2005). A Graph-Theoretic Approach to Steganography. In J. Dittmann, S. Katzenbeisser, & A. Uhl (Eds.), 9th IFIP Conference on Communications and Multimedia Security (CMS 2005) (pp. 119–128). Springer. http://hdl.handle.net/20.500.12708/51077
  • Abstracting from the Propositional Structure of First-Order Proofs / Hetzl, S., & Leitsch, A. (2005). Abstracting from the Propositional Structure of First-Order Proofs. Paris-Vienna Workshop 2005, Paris, EU. http://hdl.handle.net/20.500.12708/84469
  • Cut-Elimination: Experiments with CERES / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2005). Cut-Elimination: Experiments with CERES. Second Florence-Vienna Workshop on Logic and Computation, Florence, Italy, Austria. http://hdl.handle.net/20.500.12708/84468
  • Cut-Elimination: Experiments with CERES / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2005). Cut-Elimination: Experiments with CERES. In LOgic for Programming, Artificial Intelligence, and Reasoning (pp. 481–495). Springer, LNAI. http://hdl.handle.net/20.500.12708/51011

2004

 

  • Subsystems of open induction / Weiser, J. (2024). Subsystems of open induction [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2025.122980
    Download: PDF (1.17 MB)
  • Grammatical complexity of finite languages / Wolfsteiner, S. P. (2020). Grammatical complexity of finite languages [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.80501
    Download: PDF (1.27 MB)
  • Zyklische Superposition und Induktion / Vierling, J. (2018). Zyklische Superposition und Induktion [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.51282
    Download: PDF (913 KB)