Herbrand sequent extraction. Zbl 1166.68347
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno |
|
2008
|
Algorithmic introduction of quantified cuts. Zbl 1393.03050
Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel |
|
2014
|
Towards algorithmic cut-introduction. Zbl 1352.68213
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel |
|
2012
|
CERES: An analysis of Fürstenberg’s proof of the infinity of primes. Zbl 1181.68264
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik |
|
2008
|
Cut-elimination: experiments with CERES. Zbl 1108.03305
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik |
|
2005
|
Introducing quantified cuts in logic with equality. Zbl 1423.68418
Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Tapolczai, Janos; Weller, Daniel |
|
2014
|
Applying tree languages in proof theory. Zbl 1350.68170
Hetzl, Stefan |
|
2012
|
Inductive theorem proving based on tree grammars. Zbl 1386.03018
Eberhard, Sebastian; Hetzl, Stefan |
|
2015
|
On the complexity of proof deskolemization. Zbl 1345.03104
Baaz, Matthias; Hetzl, Stefan; Weller, Daniel |
|
2012
|
System description: GAPT 2.0. Zbl 1475.68433
Ebner, Gabriel; Hetzl, Stefan; Reis, Giselle; Riener, Martin; Wolfsteiner, Simon; Zivota, Sebastian |
|
2016
|
Proof transformation by CERES. Zbl 1125.03012
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik |
|
2006
|
Herbrand disjunctions, cut elimination and context-free tree grammars. Zbl 1366.03235
Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E. |
|
2015
|
Some observations on the logical foundations of inductive theorem proving. Zbl 1460.03005
Hetzl, Stefan; Wong, Tin Lok |
|
2017
|
A multi-focused proof system isomorphic to expansion proofs. Zbl 1403.03118
Chaudhuri, Kaustuv; Hetzl, Stefan; Miller, Dale |
|
2016
|
Compressibility of finite languages by grammars. Zbl 1390.68388
Eberhard, Sebastian; Hetzl, Stefan |
|
2015
|
On the compressibility of finite languages and formal proofs. Zbl 1390.68389
Eberhard, Sebastian; Hetzl, Stefan |
|
2018
|
CERES in higher-order logic. Zbl 1259.03071
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel |
|
2011
|
Expansion trees with cut. Zbl 1456.03085
Aschieri, Federico; Hetzl, Stefan; Weller, Daniel |
|
2019
|
On the non-confluence of cut-elimination. Zbl 1220.03048
Baaz, Matthias; Hetzl, Stefan |
|
2011
|
On the generation of quantified lemmas. Zbl 1459.03011
Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel |
|
2019
|
Understanding resolution proofs through Herbrand’s theorem. Zbl 1401.03038
Hetzl, Stefan; Libal, Tomer; Riener, Martin; Rukhaia, Mikheil |
|
2013
|
Herbrand’s theorem as higher order recursion. Zbl 1464.03085
Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E. |
|
2020
|
Herbrand confluence for first-order proofs with \(\Pi_2\)-cuts. Zbl 1433.03133
Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E. |
|
2016
|
Clause set cycles and induction. Zbl 1516.03006
Hetzl, Stefan; Vierling, Jannik |
|
2020
|
A systematic approach to canonicity in the classical sequent calculus. Zbl 1252.03128
Chaudhuri, Kaustuv; Hetzl, Stefan; Miller, Dale |
|
2012
|
Herbrand-confluence for cut elimination in classical first order logic. Zbl 1252.03123
Hetzl, Stefan; Straßburger, Lutz |
|
2012
|
Algorithmic compression of finite tree languages by rigid acyclic grammars. Zbl 1407.68251
Eberhard, Sebastian; Ebner, Gabriel; Hetzl, Stefan |
|
2017
|
Proof transformations and structural invariance. Zbl 1123.03050
Hetzl, Stefan; Leitsch, Alexander |
|
2007
|
A clausal approach to proof analysis in second-order logic. Zbl 1211.03018
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno |
|
2009
|
Describing proofs by short tautologies. Zbl 1172.03027
Hetzl, Stefan |
|
2009
|
A sequent calculus with implicit term representation. Zbl 1287.03100
Hetzl, Stefan |
|
2010
|
Cover complexity of finite languages. Zbl 1435.68166
Hetzl, Stefan; Wolfsteiner, Simon |
|
2018
|
Complexity of decision problems on totally rigid acyclic tree grammars. Zbl 1517.68160
Eberhard, Sebastian; Ebner, Gabriel; Hetzl, Stefan |
|
2018
|
The computational content of arithmetical proofs. Zbl 1269.03055
Hetzl, Stefan |
|
2012
|
Herbrand-confluence. Zbl 1325.03069
Hetzl, Stefan; Straßburger, Lutz |
|
2013
|
On the Herbrand content of LK. Zbl 1482.03014
Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E. |
|
2016
|
Unprovability results for clause set cycles. Zbl 1540.03024
Hetzl, Stefan; Vierling, Jannik |
|
2022
|
Induction and Skolemization in saturation theorem proving. Zbl 07601550
Hetzl, Stefan; Vierling, Jannik |
|
2023
|
On the form of witness terms. Zbl 1205.03064
Hetzl, Stefan |
|
2010
|
Project presentation: algorithmic structuring and compression of proofs (ASCOP). Zbl 1360.68752
Hetzl, Stefan |
|
2012
|
Induction and Skolemization in saturation theorem proving. Zbl 07601550
Hetzl, Stefan; Vierling, Jannik |
|
2023
|
Unprovability results for clause set cycles. Zbl 1540.03024
Hetzl, Stefan; Vierling, Jannik |
|
2022
|
Herbrand’s theorem as higher order recursion. Zbl 1464.03085
Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E. |
|
2020
|
Clause set cycles and induction. Zbl 1516.03006
Hetzl, Stefan; Vierling, Jannik |
|
2020
|
Expansion trees with cut. Zbl 1456.03085
Aschieri, Federico; Hetzl, Stefan; Weller, Daniel |
|
2019
|
On the generation of quantified lemmas. Zbl 1459.03011
Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel |
|
2019
|
On the compressibility of finite languages and formal proofs. Zbl 1390.68389
Eberhard, Sebastian; Hetzl, Stefan |
|
2018
|
Cover complexity of finite languages. Zbl 1435.68166
Hetzl, Stefan; Wolfsteiner, Simon |
|
2018
|
Complexity of decision problems on totally rigid acyclic tree grammars. Zbl 1517.68160
Eberhard, Sebastian; Ebner, Gabriel; Hetzl, Stefan |
|
2018
|
Some observations on the logical foundations of inductive theorem proving. Zbl 1460.03005
Hetzl, Stefan; Wong, Tin Lok |
|
2017
|
Algorithmic compression of finite tree languages by rigid acyclic grammars. Zbl 1407.68251
Eberhard, Sebastian; Ebner, Gabriel; Hetzl, Stefan |
|
2017
|
System description: GAPT 2.0. Zbl 1475.68433
Ebner, Gabriel; Hetzl, Stefan; Reis, Giselle; Riener, Martin; Wolfsteiner, Simon; Zivota, Sebastian |
|
2016
|
A multi-focused proof system isomorphic to expansion proofs. Zbl 1403.03118
Chaudhuri, Kaustuv; Hetzl, Stefan; Miller, Dale |
|
2016
|
Herbrand confluence for first-order proofs with \(\Pi_2\)-cuts. Zbl 1433.03133
Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E. |
|
2016
|
On the Herbrand content of LK. Zbl 1482.03014
Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E. |
|
2016
|
Inductive theorem proving based on tree grammars. Zbl 1386.03018
Eberhard, Sebastian; Hetzl, Stefan |
|
2015
|
Herbrand disjunctions, cut elimination and context-free tree grammars. Zbl 1366.03235
Afshari, Bahareh; Hetzl, Stefan; Leigh, Graham E. |
|
2015
|
Compressibility of finite languages by grammars. Zbl 1390.68388
Eberhard, Sebastian; Hetzl, Stefan |
|
2015
|
Algorithmic introduction of quantified cuts. Zbl 1393.03050
Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel |
|
2014
|
Introducing quantified cuts in logic with equality. Zbl 1423.68418
Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Tapolczai, Janos; Weller, Daniel |
|
2014
|
Understanding resolution proofs through Herbrand’s theorem. Zbl 1401.03038
Hetzl, Stefan; Libal, Tomer; Riener, Martin; Rukhaia, Mikheil |
|
2013
|
Herbrand-confluence. Zbl 1325.03069
Hetzl, Stefan; Straßburger, Lutz |
|
2013
|
Towards algorithmic cut-introduction. Zbl 1352.68213
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel |
|
2012
|
Applying tree languages in proof theory. Zbl 1350.68170
Hetzl, Stefan |
|
2012
|
On the complexity of proof deskolemization. Zbl 1345.03104
Baaz, Matthias; Hetzl, Stefan; Weller, Daniel |
|
2012
|
A systematic approach to canonicity in the classical sequent calculus. Zbl 1252.03128
Chaudhuri, Kaustuv; Hetzl, Stefan; Miller, Dale |
|
2012
|
Herbrand-confluence for cut elimination in classical first order logic. Zbl 1252.03123
Hetzl, Stefan; Straßburger, Lutz |
|
2012
|
The computational content of arithmetical proofs. Zbl 1269.03055
Hetzl, Stefan |
|
2012
|
Project presentation: algorithmic structuring and compression of proofs (ASCOP). Zbl 1360.68752
Hetzl, Stefan |
|
2012
|
CERES in higher-order logic. Zbl 1259.03071
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel |
|
2011
|
On the non-confluence of cut-elimination. Zbl 1220.03048
Baaz, Matthias; Hetzl, Stefan |
|
2011
|
A sequent calculus with implicit term representation. Zbl 1287.03100
Hetzl, Stefan |
|
2010
|
On the form of witness terms. Zbl 1205.03064
Hetzl, Stefan |
|
2010
|
A clausal approach to proof analysis in second-order logic. Zbl 1211.03018
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno |
|
2009
|
Describing proofs by short tautologies. Zbl 1172.03027
Hetzl, Stefan |
|
2009
|
Herbrand sequent extraction. Zbl 1166.68347
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno |
|
2008
|
CERES: An analysis of Fürstenberg’s proof of the infinity of primes. Zbl 1181.68264
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik |
|
2008
|
Proof transformations and structural invariance. Zbl 1123.03050
Hetzl, Stefan; Leitsch, Alexander |
|
2007
|
Proof transformation by CERES. Zbl 1125.03012
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik |
|
2006
|
Cut-elimination: experiments with CERES. Zbl 1108.03305
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik |
|
2005
|