Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E. Herbrand’s theorem as higher order recursion. (English) Zbl 1464.03085 Ann. Pure Appl. Logic 171, No. 6, Article ID 102792, 45 p. (2020). Reviewer: Annika Kanckos (Helsinki) MSC: 03F05 03F07 03D05 03F30 PDFBibTeX XMLCite \textit{B. Afshari} et al., Ann. Pure Appl. Logic 171, No. 6, Article ID 102792, 45 p. (2020; Zbl 1464.03085) Full Text: DOI
Aschieri, Federico; Hetzl, Stefan; Weller, Daniel Expansion trees with cut. (English) Zbl 1456.03085 Math. Struct. Comput. Sci. 29, No. 8, 1009-1029 (2019). MSC: 03F05 PDFBibTeX XMLCite \textit{F. Aschieri} et al., Math. Struct. Comput. Sci. 29, No. 8, 1009--1029 (2019; Zbl 1456.03085) Full Text: DOI arXiv
Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel On the generation of quantified lemmas. (English) Zbl 1459.03011 J. Autom. Reasoning 63, No. 1, 95-126 (2019). MSC: 03B35 03F05 68V15 PDFBibTeX XMLCite \textit{G. Ebner} et al., J. Autom. Reasoning 63, No. 1, 95--126 (2019; Zbl 1459.03011) Full Text: DOI
Hetzl, Stefan; Wong, Tin Lok Some observations on the logical foundations of inductive theorem proving. (English) Zbl 1460.03005 Log. Methods Comput. Sci. 13, No. 4, Paper No. 10, 26 p. (2017). MSC: 03B35 03C62 03F05 PDFBibTeX XMLCite \textit{S. Hetzl} and \textit{T. L. Wong}, Log. Methods Comput. Sci. 13, No. 4, Paper No. 10, 26 p. (2017; Zbl 1460.03005) Full Text: DOI arXiv
Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E. Herbrand confluence for first-order proofs with \(\Pi_2\)-cuts. (English) Zbl 1433.03133 Probst, Dieter (ed.) et al., Concepts of proof in mathematics, philosophy, and computer science. Based on the Humboldt-Kolleg, Bern, Switzerland, September 9–13, 2013. Ontos Mathematical Logic 6. Berlin: De Gruyter. 5-40 (2016). MSC: 03F05 68Q42 03F07 PDFBibTeX XMLCite \textit{B. Afshari} et al., Ontos Math. Log. 6, 5--40 (2016; Zbl 1433.03133) Full Text: DOI
Chaudhuri, Kaustuv; Hetzl, Stefan; Miller, Dale A multi-focused proof system isomorphic to expansion proofs. (English) Zbl 1403.03118 J. Log. Comput. 26, No. 2, 577-603 (2016). MSC: 03F07 03B10 03F03 03F05 PDFBibTeX XMLCite \textit{K. Chaudhuri} et al., J. Log. Comput. 26, No. 2, 577--603 (2016; Zbl 1403.03118) Full Text: DOI
Hetzl, Stefan; Zivota, Sebastian Tree grammars for the elimination of non-prenex cuts. (English) Zbl 1373.03123 Kreutzer, Stephan (ed.), 24th EACSL annual conference and 29th workshop on computer science logic, CSL’15, Berlin, Germany, September 7–10, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-90-3). LIPIcs – Leibniz International Proceedings in Informatics 41, 110-127 (2015). MSC: 03F05 68Q42 PDFBibTeX XMLCite \textit{S. Hetzl} and \textit{S. Zivota}, LIPIcs -- Leibniz Int. Proc. Inform. 41, 110--127 (2015; Zbl 1373.03123) Full Text: DOI
Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E. Herbrand disjunctions, cut elimination and context-free tree grammars. (English) Zbl 1366.03235 Altenkirch, Thorsten (ed.), 13th international conference on typed lambda calculi and applications, TLCA’15, Warsaw, Poland, July 1–3, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-87-3). LIPIcs – Leibniz International Proceedings in Informatics 38, 1-16 (2015). MSC: 03F05 03D05 68Q42 PDFBibTeX XMLCite \textit{B. Afshari} et al., LIPIcs -- Leibniz Int. Proc. Inform. 38, 1--16 (2015; Zbl 1366.03235) Full Text: DOI
Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel Algorithmic introduction of quantified cuts. (English) Zbl 1393.03050 Theor. Comput. Sci. 549, 1-16 (2014). MSC: 03F05 PDFBibTeX XMLCite \textit{S. Hetzl} et al., Theor. Comput. Sci. 549, 1--16 (2014; Zbl 1393.03050) Full Text: DOI arXiv
Hetzl, Stefan; Straßburger, Lutz Herbrand-confluence. (English) Zbl 1325.03069 Log. Methods Comput. Sci. 9, No. 4, Paper No. 26, 25 p. (2013). Reviewer: Andrzej Indrzejczak (Łódź) MSC: 03F05 PDFBibTeX XMLCite \textit{S. Hetzl} and \textit{L. Straßburger}, Log. Methods Comput. Sci. 9, No. 4, Paper No. 26, 25 p. (2013; Zbl 1325.03069) Full Text: DOI arXiv
Hetzl, Stefan The computational content of arithmetical proofs. (English) Zbl 1269.03055 Notre Dame J. Formal Logic 53, No. 3, 289-296 (2012). Reviewer: G. E. Mints (Stanford) MSC: 03F05 03F07 03F30 PDFBibTeX XMLCite \textit{S. Hetzl}, Notre Dame J. Formal Logic 53, No. 3, 289--296 (2012; Zbl 1269.03055) Full Text: DOI Euclid
Hetzl, Stefan; Straßburger, Lutz Herbrand-confluence for cut elimination in classical first order logic. (English) Zbl 1252.03123 Cégielski, Patrick (ed.) et al., Computer science logic (CSL’12). 26th international workshop, 21th annual conference of the EACSL, September 3–6, 2012, Fontainebleau, France. Selected papers based on the presentations at the conference. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-42-2). LIPIcs – Leibniz International Proceedings in Informatics 16, 320-334, electronic only (2012). MSC: 03F05 03B10 03D05 68Q42 PDFBibTeX XMLCite \textit{S. Hetzl} and \textit{L. Straßburger}, LIPIcs -- Leibniz Int. Proc. Inform. 16, 320--334 (2012; Zbl 1252.03123) Full Text: DOI
Baaz, Matthias; Hetzl, Stefan; Weller, Daniel On the complexity of proof deskolemization. (English) Zbl 1345.03104 J. Symb. Log. 77, No. 2, 669-686 (2012). MSC: 03F20 03F05 PDFBibTeX XMLCite \textit{M. Baaz} et al., J. Symb. Log. 77, No. 2, 669--686 (2012; Zbl 1345.03104) Full Text: DOI Euclid
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel Towards algorithmic cut-introduction. (English) Zbl 1352.68213 Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 228-242 (2012). MSC: 68T15 03F05 PDFBibTeX XMLCite \textit{S. Hetzl} et al., Lect. Notes Comput. Sci. 7180, 228--242 (2012; Zbl 1352.68213) Full Text: DOI
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel CERES in higher-order logic. (English) Zbl 1259.03071 Ann. Pure Appl. Logic 162, No. 12, 1001-1034 (2011). Reviewer: G. E. Mints (Stanford) MSC: 03F05 03F07 03B15 PDFBibTeX XMLCite \textit{S. Hetzl} et al., Ann. Pure Appl. Logic 162, No. 12, 1001--1034 (2011; Zbl 1259.03071) Full Text: DOI
Baaz, Matthias; Hetzl, Stefan On the non-confluence of cut-elimination. (English) Zbl 1220.03048 J. Symb. Log. 76, No. 1, 313-340 (2011). Reviewer: Henry Towsner (Los Angeles) MSC: 03F05 PDFBibTeX XMLCite \textit{M. Baaz} and \textit{S. Hetzl}, J. Symb. Log. 76, No. 1, 313--340 (2011; Zbl 1220.03048) Full Text: DOI
Hetzl, Stefan A sequent calculus with implicit term representation. (English) Zbl 1287.03100 Dawar, Anuj (ed.) et al., Computer science logic. 24th international workshop, CSL 2010, 19th annual conference of the EACSL, Brno, Czech Republic, August 23–27, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-15204-7/pbk). Lecture Notes in Computer Science 6247, 351-365 (2010). MSC: 03F05 PDFBibTeX XMLCite \textit{S. Hetzl}, Lect. Notes Comput. Sci. 6247, 351--365 (2010; Zbl 1287.03100) Full Text: DOI HAL
Hetzl, Stefan On the form of witness terms. (English) Zbl 1205.03064 Arch. Math. Logic 49, No. 5, 529-554 (2010). Reviewer: Saeed Salehi (Tabriz) MSC: 03F05 03F07 03F30 PDFBibTeX XMLCite \textit{S. Hetzl}, Arch. Math. Logic 49, No. 5, 529--554 (2010; Zbl 1205.03064) Full Text: DOI HAL
Hetzl, Stefan Describing proofs by short tautologies. (English) Zbl 1172.03027 Ann. Pure Appl. Logic 159, No. 1-2, 129-145 (2009). Reviewer: G. E. Mints (Stanford) MSC: 03F05 03F07 03F20 PDFBibTeX XMLCite \textit{S. Hetzl}, Ann. Pure Appl. Logic 159, No. 1--2, 129--145 (2009; Zbl 1172.03027) Full Text: DOI
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno A clausal approach to proof analysis in second-order logic. (English) Zbl 1211.03018 Artemov, Sergei (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3–6, 2009. Proceedings. Berlin: Springer (ISBN 978-3-540-92686-3/pbk). Lecture Notes in Computer Science 5407, 214-229 (2009). MSC: 03B15 03F05 PDFBibTeX XMLCite \textit{S. Hetzl} et al., Lect. Notes Comput. Sci. 5407, 214--229 (2009; Zbl 1211.03018) Full Text: DOI
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik CERES: An analysis of Fürstenberg’s proof of the infinity of primes. (English) Zbl 1181.68264 Theor. Comput. Sci. 403, No. 2-3, 160-175 (2008). MSC: 68T15 PDFBibTeX XMLCite \textit{M. Baaz} et al., Theor. Comput. Sci. 403, No. 2--3, 160--175 (2008; Zbl 1181.68264) Full Text: DOI
Hetzl, Stefan; Leitsch, Alexander Proof transformations and structural invariance. (English) Zbl 1123.03050 Aguzzoli, Stefano (ed.) et al., Algebraic and proof-theoretic aspects of non-classical logics. Papers in honor of Daniele Mundici on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-540-75938-6/pbk). Lecture Notes in Computer Science 4460. Lecture Notes in Artificial Intelligence, 201-230 (2007). MSC: 03F07 03F05 PDFBibTeX XMLCite \textit{S. Hetzl} and \textit{A. Leitsch}, Lect. Notes Comput. Sci. 4460, 201--230 (2007; Zbl 1123.03050) Full Text: DOI
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik Proof transformation by CERES. (English) Zbl 1125.03012 Borwein, Jonathan M. (ed.) et al., Mathematical knowledge management. 5th international conference, MKM 2006, Wokingham, UK, August 11–12, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37104-4/pbk). Lecture Notes in Computer Science 4108. Lecture Notes in Artificial Intelligence, 82-93 (2006). MSC: 03B35 03F05 68T15 PDFBibTeX XMLCite \textit{M. Baaz} et al., Lect. Notes Comput. Sci. 4108, 82--93 (2006; Zbl 1125.03012) Full Text: DOI
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik Cut-elimination: experiments with CERES. (English) Zbl 1108.03305 Baader, Franz (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14–18, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25236-3/pbk). Lecture Notes in Computer Science 3452. Lecture Notes in Artificial Intelligence, 481-495 (2005). MSC: 03B35 03F05 68T15 PDFBibTeX XMLCite \textit{M. Baaz} et al., Lect. Notes Comput. Sci. 3452, 481--495 (2005; Zbl 1108.03305) Full Text: DOI