Stefan Hetzl
Associate Prof. Dipl.-Ing. Dr.techn. / BSc
Research Areas
- Interactive theorem proving, Automated theorem proving, Proof Theory, Theory of formal Languages
About
Computational Logic, Proof Theory, Theory of Formal Languages, Automated theorem proving, Interactive theorem proving
Role
-
Affilliated
Theory and Logic, E192-05
Courses
2020W
- Bachelor Thesis for Informatics and Business Informatics / 185.A26 / PR
- Project in Computer Science 1 / 185.A36 / PR
- Project in Computer Science 2 / 185.A37 / PR
- Research Seminar for Master and PhD students / 185.A39 / SE
2021S
- Bachelor Thesis for Informatics and Business Informatics / 185.A26 / PR
- Project in Computer Science 1 / 185.A36 / PR
- Project in Computer Science 2 / 185.A37 / PR
- Research Seminar for Master and PhD students / 185.A39 / SE
Projects
-
Structure and Expressivity: The Mathematical Foundations of Inductive Reasoning
2013 – 2021 / Vienna Science and Technology Fund (WWFT) -
Algorithmic Structuring and Compression of Proofs
2013 – 2018 / Austrian Science Fund (FWF) -
Automated Analysis of Mathematical Proofs
2005 – 2007 / Austrian Science Fund (FWF)
Publications
2019
- Expansion trees with cut / F. Aschieri, S. Hetzl, D. Weller / Mathematical Structures In Computer Science, 29 (2019), 8; 1009 - 1029
- On the Generation of Quantified Lemmas / G. Ebner, S. Hetzl, A. Leitsch, G. Reis, D. Weller / Journal of Automated Reasoning, 63 (2019), 1; 95 - 126
2016
- System Description: GAPT 2.0 / S. Hetzl, G. Reis, M. Riener, S. Wolfsteiner, S. Zivota, G. Ebner / Talk: International Joint Conference on Automated Reasoning, Coimbra, Portugal; 2016-06-27 - 2016-07-02
- System Description: GAPT 2.0 / G. Ebner, S. Hetzl, G. Reis, M. Riener, S. Wolfsteiner, S. Zivota / Lecture Notes in Computer Science, 9706 (2016), 293 - 301
2014
- Algorithmic introduction of quantified cuts / S. Hetzl, A. Leitsch, G. Reis, D. Weller / Theoretical Computer Science, 549 (2014), 1 - 16
- Introducing Quantified Cuts in Logic with Equality / S. Hetzl, A. Leitsch, G. Reis, J. Tapolczai, D. Weller / in: "Automated Reasoning - 7th International Joint Conference", issued by: IJCAR; LNCS 8562, Springer, 2014, 240 - 254
- Preface / A. Ciabattoni, M. Baaz, D.M. Gabbay, S. Hetzl, D. Weller / Journal of Logic and Computation, 1 (2014)
- Algorithmic Introduction of Quantified Cuts / S. Hetzl, G. Reis, D. Weller / CoRR - Computing Research Repository, abs/1401.4330 (2014), 38 pages
- Introducing Quantified Cuts in Logic with Equality / A. Leitsch, S. Hetzl, G. Reis, D. Weller et al. / CoRR - Computing Research Repository, abs/1402.2474 (2014), abs/1402.2474; 16 pages
2013
- Expansion Trees with Cut / D. Weller, S. Hetzl / CoRR - Computing Research Repository, abs/1308.0428 (2013), abs/1308.0428; 1 - 25
- Herbrand-Confluence / S. Hetzl, L. Strassburger / Logical Methods in Computer Science, 9 (2013), 4; 1 - 25
2012
- Towards Algorithmic Cut-Introduction / A. Leitsch, S. Hetzl, D. Weller / in: "Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18", N. Bjorner, A. Voronkov (ed.); Springer LNCS, 2012, ISBN: 978-3-642-28716-9, 228 - 242
2011
- Ceres in higher-order logic / S. Hetzl, A. Leitsch, D. Weller / Annals of Pure and Applied Logic, 162 (2011), 12; 1001 - 1034
- On the non-confluence of cut-elimination / M. Baaz, S. Hetzl / Journal of Symbolic Logic, 76 (2011), 1; 313 - 340
2010
- On the complexity of proof deskolemization / M. Baaz, S. Hetzl, D. Weller / Talk: Collegium Locicum 2010: Proofs and Structures, Paris; 2010-11-08 - 2010-11-10
- CERES in higher-order-logic / S. Hetzl, A. Leitsch, D. Weller / Talk: Workshop on Classical Logic and Computation (CL&C'10), Brünn; 2010-08-22
2009
- A Clausal Approach to Proof Analysis in Second-Order Logic / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / Talk: Symposium on Logical Foundations of Computer Science (LFCS 2009), Deerfield Beach, FL, USA; 2009-01-03 - 2009-01-06; in: "Logical Foundations of Computer Science", A. Nerode, S. Artemov (ed.); Springer, LNCS, 5407 (2009), ISBN: 3-540-92686-0; 214 - 229
- A Clausal Approach to Proof Analysis in Second-Order Logic / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / in: "Lecture Notes in Computer Science, 5407", E. Artemov, A. Nerode (ed.); Springer LNCS, Heidelberg, 2009, ISBN: 3-540-92686-0, 214 - 229
2008
- Transforming and Analyzing Proofs in the CERES-system / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / Talk: The LPAR 2008 Workshops: KEAPPA and IWIL 2008, Doha, Qatar; 2008-11-22; in: "Proceedings of the LPAR 2008 Workshops", P. Rudnicki, G. Sutcliffe et al. (ed.); CEUR-WS.org, Vol 418 (2008), ISSN: 1613-0073; 77 - 91
- Cut-elimination / M. Baaz, S. Hetzl / Talk: Third Vienna Tbilisi Summer School in Logic and Language, Tbilisi, Georgia (invited); 2008-09-24 - 2008-09-28
- CERES: An analysis of Fürstenberg's proof of the infinity of primes / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / Theoretical Computer Science, 403 (2008), 2-3; 160 - 175
- Herbrand Sequent Extraction / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / in: "AISC/Calculemus/MKM 2008", S. Autexier et al. (ed.); Springer, Heidelberg, 2008, ISBN: 9783540851097, 462 - 477
- Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / in: "Proceedings of the CICIM Workshops on ESARM-08", G. Sutcliffe, S. Colton, S. Schulz (ed.); issued by: Ceur Workshop Proceedings; CEUR-WS.org, 2008, ISSN: 1613-0073, 23 - 41
2007
- Characteristic Clause Sets and Proof Transformations / Doctoral Thesis by S. Hetzl / Supervisor, Reviewer: A. Leitsch, M. Baaz; Institut für Computersprachen E185/2, 2007; oral examination: 2007-06-14
- Proof Transformations and Structural Invariance / A. Leitsch, S. Hetzl / in: "LNAI 4460: Algebraic and Proof-theoretic Aspects", S. Aguzzoli et al. (ed.); Springer, LNAI 4460, 2007, 201 - 230
2006
- Comparing Mathematical Proofs / S. Hetzl / Talk: Studia Logica International Conference; Towards Mathematical Philosophy; Trends in Logic IV, Torun, Poland; 2006-09-01 - 2006-09-04
- System Description: The Cut-Elimination System CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / Talk: FLoC'06 Workshop on Empirically Successful Computerized Reasoning (ESCoR), Seattle, USA; 2006-08-21; in: "ESCoR 2006 Empirically Successful Computerized Reasoning", G. Sutcliffe, R. Schmidt, S. Schulz (ed.); CEUR Workshop Proceedings, 192 (2006), ISSN: 1613-0073; Paper ID 11, 9 pages
- A Similarity Criterion for Proofs (abstract) / S. Hetzl / Talk: Computability in Europe 2006, Logical Approaches to Computational Barriers, Swansea, Wales; 2006-06-30 - 2006-07-05; in: "Logical Approaches to Computational Barriers", A. Beckmann, U. Berger, B. Löwe, J. Tucker (ed.); University of Wales Swansea Report Series, CSR 7-2006 (2006), ISBN: 0-86076-189-4; - 295
- Proof transformation by CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / Lecture Notes in Computer Science, 4108 (2006), 82 - 93
- Proof Transformation by CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / in: "MKM 2006", J.M. Borwein, W.M. Farmer (ed.); Springer, Berlin Heidelberg, 2006, 82 - 93
2005
- Abstracting from the Propositional Structure of First-Order Proofs / S. Hetzl, A. Leitsch / Talk: Paris-Vienna Workshop 2005, Paris; 2005-12-19
- Cut-Elimination: Experiments with CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / Talk: Second Florence-Vienna Workshop on Logic and Computation, Florenz; 2005-11-02 - 2005-11-05
- Cut-Elimination: Experiments with CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / in: "LOgic for Programming, Artificial Intelligence, and Reasoning", issued by: Franz Baader, Andrei Voronkov; Springer, LNAI, Heidelberg, 2005, ISBN: 3-540-25236-3, 481 - 495
- A Graph-Theoretic Approach to Steganography / S. Hetzl, P. Mutzel / in: "9th IFIP Conference on Communications and Multimedia Security (CMS 2005)", J. Dittmann, S. Katzenbeisser, A. Uhl (ed.); issued by: International Federation for Information Processing; Springer, LNCS 3677, 2005, ISBN: 3-540-28791-4, 119 - 128