Wissenschaftliche Artikel

Hetzl, S., & Vierling, J. (2020). Clause Set Cycles and Induction. Logical Methods in Computer Science, 16(4). https://doi.org/10.23638/LMCS-16(4:11)2020 ( reposiTUm)
Hetzl, S., & Zivota, S. (2020). Decidability of affine solution problems. Journal of Logic and Computation, 30(3), 697–714. https://doi.org/10.1093/logcom/exz033 ( reposiTUm)
Afshari, B., Hetzl, S., & Leigh, G. E. (2020). Herbrand’s theorem as higher order recursion. Annals of Pure and Applied Logic, 171, Article 102792. https://doi.org/10.1016/j.apal.2020.102792 ( reposiTUm)
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 ( reposiTUm)
Ebner, G., Hetzl, S., Leitsch, A., Reis, G., & Weller, D. (2019). On the Generation of Quantified Lemmas. Journal of Automated Reasoning, 63, 95–126. https://doi.org/10.1007/s10817-018-9462-8 ( reposiTUm)
Eberhard, S., & Hetzl, S. (2018). On the Compressibility of Finite Languages and Formal Proofs. Information and Computation, 259, 191–213. https://doi.org/10.1016/j.ic.2017.09.001 ( reposiTUm)
Hetzl, S., & Wong, T. L. (2018). Some observations on the logical foundations of inductive theorem proving. Logical Methods in Computer Science, 13(4). https://doi.org/10.23638/LMCS-13(4:10)2017 ( reposiTUm)
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 ( reposiTUm)
Eberhard, S., Ebner, G., & Hetzl, S. (2017). Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars. ACM Transactions on Computational Logic, 18(4), 1–20. https://doi.org/10.1145/3127401 ( reposiTUm)
Eberhard, S., Hetzl, S., & Weller, D. (2017). Boolean Unification with Predicates. Journal of Logic and Computation, 27(1), 109–128. https://doi.org/10.1093/logcom/exv059 ( reposiTUm)
Chaudhuri, K., Hetzl, S., & Miller, D. (2016). A multi-focused proof system isomorphic to expansion proof. Journal of Logic and Computation, 26(2), 577–603. https://doi.org/10.1093/logcom/exu030 ( reposiTUm)
Afshari, B., Hetzl, S., & Leigh, G. E. (2016). On the Herbrand content of LK. Electronic Proceedings in Theoretical Computer Science, 213, 1–10. https://doi.org/10.4204/eptcs.213.1 ( reposiTUm)
Eberhard, S., & Hetzl, S. (2015). Compressibility of Finite Languages by Grammars. Descriptional Complexity of Formal Systems, 93–104. https://doi.org/10.1007/978-3-319-19225-3_8 ( reposiTUm)
Eberhard, S., & Hetzl, S. (2015). Inductive theorem proving based on tree grammars. Annals of Pure and Applied Logic, 166(6), 665–700. https://doi.org/10.1016/j.apal.2015.01.002 ( reposiTUm)
Adelsberger, S., Hetzl, S., & Miller, D. (2014). The Cayley-Hamilton Theorem. Archive of Formal Proofs, 2014. http://hdl.handle.net/20.500.12708/157702 ( reposiTUm)
Hetzl, S., Leitsch, A., Reis, G., & Weller, D. (2014). Algorithmic introduction of quantified cuts. Theoretical Computer Science, 549, 1–16. https://doi.org/10.1016/j.tcs.2014.05.018 ( reposiTUm)
Hetzl, S., & Strassburger, L. (2013). Herbrand-Confluence. Logical Methods in Computer Science, 9(4). https://doi.org/10.2168/LMCS-9(4:24)2013 ( reposiTUm)
Avigad, J., & Hetzl, S. (2012). Bondy’s Theorem. Archive of Formal Proofs, XX(1), 3. http://hdl.handle.net/20.500.12708/165046 ( reposiTUm)
Hetzl, S. (2012). The computational content of arithmetical proofs. Notre Dame Journal of Formal Logic, 53(3). https://doi.org/10.1215/00294527-1716811 ( reposiTUm)
Baaz, M., Hetzl, S., & Weller, D. (2012). On the complexity of proof deskolemization. Journal of Symbolic Logic, 77(2), 669–686. https://doi.org/10.2178/jsl/1333566645 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)

Beiträge in Tagungsbänden

Eberhard, S., Ebner, G., & Hetzl, S. (2018). Complexity of decision problems on totally rigid acyclic tree grammars. In Developments in Language Theory, LNCS 2018 (pp. 291–303). Springer. http://hdl.handle.net/20.500.12708/41673 ( reposiTUm)
Hetzl, S., & Wolfsteiner, S. (2018). Cover Complexity of Finite Languages. In Descriptional Complexity of Formal Systems (pp. 139–150). Springer. https://doi.org/10.1007/978-3-319-94631-3_12 ( reposiTUm)
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 ( reposiTUm)
Hetzl, S., & Zivota, S. (2015). Tree Grammars for the Elimination of Non-prenex Cuts. In S. Kreutzer (Ed.), 24th EACSL Annual Conference on Computer Science Logic - CLS 2015 (pp. 110–127). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CSL.2015.110 ( reposiTUm)
Afshari, B., Hetzl, S., & Leigh, G. (2015). Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars. In T. Altenkirch (Ed.), 13th International Conference on Typed Lambda Calculi and Applications - TLCA 2015 (pp. 1–16). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.TLCA.2015.1 ( reposiTUm)
Hetzl, S., Leitsch, A., Reis, G., Tapolczai, J., & Weller, D. (2014). Introducing Quantified Cuts in Logic with Equality. In Automated Reasoning (pp. 240–254). LNCS 8562. https://doi.org/10.1007/978-3-319-08587-6_17 ( reposiTUm)
Hetzl, S., Libal, T., Riener, M., & Rukhaia, M. (2013). Understanding resolution proofs through Herbrand’s Theorem. In Automated Reasoning with Analytic Tableaux and Related Methods. 22th International Conference, TABLEAUX 2013, Nancy, France, EU. Lecture Notes in Computer Science/Springer. https://doi.org/10.1007/978-3-642-40537-2_15 ( reposiTUm)
Hetzl, S. (2012). Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP). In Intelligent Computer Mathematics (pp. 438–442). Springer Verlag. https://doi.org/10.1007/978-3-642-31374-5_32 ( reposiTUm)
Hetzl, S. (2012). Applying Tree Languages in Proof Theory. In Language and Automata Theory and Applications (pp. 301–312). Springer. https://doi.org/10.1007/978-3-642-28332-1_26 ( reposiTUm)
Chaudhuri, K., Hetzl, S., & Miller, D. (2012). A systematic approach to canonicity in the classical sequent calculus. In P. Cegielski & A. Durand (Eds.), Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL (pp. 183–187). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CSL.2012.183 ( reposiTUm)
Hetzl, S., & Straßburger, L. (2012). Herbrand-confluence for cut elimination in classical first order logic. In P. Cegielski & A. Durand (Eds.), Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL (pp. 320–334). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CSL.2012.320 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)

Beiträge in Büchern

Afshari, B., Hetzl, S., & Leigh, G. E. (2016). Herbrand Confluence for First-Order Proofs with Π2-Cuts. In Concepts of Proof in Mathematics, Philosophy, and Computer Science (pp. 5–40). Walter de Gruyter. https://doi.org/10.1515/9781501502620-003 ( reposiTUm)
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 ( reposiTUm)

Präsentationen

Hetzl, S. (2018). A simplified proof of the epsilon theorems. 3rd. FISP Workshop, Wien, Austria. http://hdl.handle.net/20.500.12708/122701 ( reposiTUm)
Hetzl, S. (2017). System Description: General Architecture for Proof Theory. Helmut Veith Memorial Workshop, Obergurgl, Austria. http://hdl.handle.net/20.500.12708/121993 ( reposiTUm)
Hetzl, S. (2017). Some Observations on the Logical Foundations of Inductive Theorem Proving. Collegium Logicum Proof Theory: Herbrand’s Theorem Revisited, Wien, Austria. http://hdl.handle.net/20.500.12708/122172 ( reposiTUm)
Hetzl, S. (2017). On the Complexity of Grammars and First-Order Proofs. Computational Logic Day, Kurt Gödel Research Centre, Vienna University, Kurt Gödel Research Centre, Vienna University, Austria. http://hdl.handle.net/20.500.12708/122170 ( reposiTUm)
Hetzl, S. (2017). Some Observations on the Logical Foundations of Inductive Theorem Proving. Mathematical Logic: Proof theory, Constructive Mathematics, Oberwolfach, Germany. http://hdl.handle.net/20.500.12708/122171 ( reposiTUm)
Hetzl, S. (2017). Hilbert’s Larger Programme. International Summer School for Proof Theory in First-Order-Logic, Funchal, Portugal. http://hdl.handle.net/20.500.12708/122305 ( reposiTUm)
Hetzl, S. (2016). Inductive theorem proving based on tree grammars. PUMA Graduiertenkolleg, München, Germany. http://hdl.handle.net/20.500.12708/121471 ( reposiTUm)
Afshari, B., Hetzl, S., & Leigh, G. (2016). On the Herbrand content of LK. First International Conference - Formal Structures for Computation and Deduction (FSCD), Porto, Portugal. http://hdl.handle.net/20.500.12708/121493 ( reposiTUm)
Hetzl, S. (2015). Compressibility of first-order proofs. Seminar of the Theory and Logic Group, Technische Universität Wien, Austria. http://hdl.handle.net/20.500.12708/121202 ( reposiTUm)
Hetzl, S. (2015). Inductive theorem proving based on tree grammars. 2nd Workshop on Automated Inductive Theorem Proving, Gothenburg, Sweden. http://hdl.handle.net/20.500.12708/121204 ( reposiTUm)
Eberhard, S., & Hetzl, S. (2015). Compressibility of finite languages by grammars. Descriptional Complexity of Formal Systems DCFS 2015, Waterloo, Ontario, Canada. http://hdl.handle.net/20.500.12708/121201 ( reposiTUm)
Hetzl, S. (2015). On the complexity of grammars and first-order proofs. Workshop on Proof Theory, Muenchenwiler, Switzerland. http://hdl.handle.net/20.500.12708/121203 ( reposiTUm)
Hetzl, S. (2013). Proofs and grammars. Logic Colloquium 2013, Evora, Portugal, EU. http://hdl.handle.net/20.500.12708/120359 ( reposiTUm)
Eberhard, S., & Hetzl, S. (2013). Guessing induction formulas for proofs of universal statements. LIX Colloquium 2013: Theory and Application of Formal Proofs, Paris, France, EU. http://hdl.handle.net/20.500.12708/120438 ( reposiTUm)
Weller, D., & Hetzl, S. (2013). Expansion trees with cut. LIX Colloquium 2013: Theory and Application of Formal Proofs, Paris, France, EU. http://hdl.handle.net/20.500.12708/120437 ( reposiTUm)
Hetzl, S. (2013). Automata and formal language theory. Ninth International Tbilisi Summer School in Logic and Language, Tbilisi, Georgia. http://hdl.handle.net/20.500.12708/120411 ( reposiTUm)
Hetzl, S. (2012). Which proofs can be computed by cut-elimination? Association For Symbolic Logic 2012 North American Annual Meeting, Wisconsin, USA, Non-EU. http://hdl.handle.net/20.500.12708/120190 ( reposiTUm)
Hetzl, S. (2012). A systematic approach to canonicity in the classical sequent calculus. Parsifal team seminar, Paris, France, EU. http://hdl.handle.net/20.500.12708/120191 ( reposiTUm)
Hetzl, S. (2012). Which proofs can be computed by cut-elimination? Mathematical Logic seminar, Carnegie Mellon University, Pennsylvania, USA, Non-EU. http://hdl.handle.net/20.500.12708/120192 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)
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 ( reposiTUm)

Preprints

Leitsch, A., Hetzl, S., Reis, G., & Weller, D. (2014). Introducing Quantified Cuts in Logic with Equality. arXiv. https://doi.org/10.48550/arXiv.1402.2474 ( reposiTUm)
Hetzl, S., Reis, G., & Weller, D. (2014). Algorithmic Introduction of Quantified Cuts. arXiv. https://doi.org/10.48550/arXiv.1401.4330 ( reposiTUm)
Hetzl, S., & Weller, D. (2013). Expansion trees with cut (p. 25). arXiv. https://doi.org/10.48550/arXiv.1308.0428 ( reposiTUm)
Hetzl, S., & Straßburger, L. (2013). Herbrand-Confluence. arXiv. https://doi.org/10.48550/arXiv.1310.8156 ( reposiTUm)

Hochschulschriften

Hetzl, S. (2012). Computational proof analysis [Professorial Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/159071 ( reposiTUm)
Hetzl, S. (2007). Characteristic clause sets and proof transformations [Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/183195 ( reposiTUm)
Hetzl, S. (2004). Projection-based cut-elimination and normalization [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-10645 ( reposiTUm)