@article(Afshari2018Herbrand,
 author       = {Bahareh Afshari and Stefan Hetzl and Graham Leigh},
 year         = {2018},
 title        = {Herbrand's Theorem as Higher Order Recursion},
 doi          = {10.14760/OWP-2018-01},
)
@inproceedings(Baaz2006Proof,
 author       = {Matthias Baaz and Stefan Hetzl and Alexander Leitsch and Clemens Richter and Hendrik Spohr},
 year         = {2006},
 title        = {Proof Transformation by {CERES}},
 editor       = {Jonathan M. Borwein and William M. Farmer},
 booktitle    = {5th International Conference on Mathematical Knowledge Management, {MKM}},
 series       = {Lecture Notes in Computer Science},
 volume       = {4108},
 publisher    = {Springer},
 pages        = {82--93},
 doi          = {10.1007/11812289_8},
)
@article(Baaz2008CERES,
 author       = {Matthias Baaz and Stefan Hetzl and Alexander Leitsch and Clemens Richter and Hendrik Spohr},
 year         = {2008},
 title        = {{CERES:} An analysis of F{\"{u}}rstenberg's proof of the infinity of primes},
 journal      = {Theoretical Computer Science},
 volume       = {403},
 number       = {2-3},
 pages        = {160--175},
 doi          = {10.1016/j.tcs.2008.02.043},
)
@article(Baaz2012complexity,
 author       = {Matthias Baaz and Stefan Hetzl and Daniel Weller},
 year         = {2012},
 title        = {On the complexity of proof deskolemization},
 journal      = {Journal of Symbolic Logic},
 volume       = {77},
 number       = {2},
 pages        = {669--686},
 doi          = {10.2178/jsl/1333566645},
)
@article(Baaz2000Cut,
 author       = {Matthias Baaz and Alexander Leitsch},
 year         = {2000},
 title        = {Cut-elimination and Redundancy-elimination by Resolution},
 journal      = {Journal of Symbolic Computation},
 volume       = {29},
 number       = {2},
 pages        = {149--177},
 doi          = {10.1006/jsco.1999.0359},
)
@article(Barbanera1996Symmetric,
 author       = {Franco Barbanera and Stefano Berardi},
 year         = {1996},
 title        = {A Symmetric Lambda Calculus for Classical Program Extraction},
 journal      = {Information and Computation},
 volume       = {125},
 number       = {2},
 pages        = {103--117},
 doi          = {10.1006/inco.1996.0025},
)
@incollection(Buss1995Herbrands,
 author       = {Samuel R. Buss},
 year         = {1995},
 title        = {{O}n {H}erbrand's {T}heorem},
 booktitle    = {Logic and Computational Complexity},
 series       = {Lecture Notes in Computer Science},
 volume       = {960},
 publisher    = {Springer},
 pages        = {195--209},
 doi          = {10.1007/3-540-60178-3_85},
)
@techreport(Cerna2018System,
 author       = {David Cerna and Anela Lolic},
 year         = {2018},
 title        = {System Description: {GAPT} for schematic proofs},
 type         = {RISC Report Series},
 url          = {http://www.risc.jku.at/publications/download/risc_5591/schematicGapt.pdf},
)
@article(Eberhard2015Inductive,
 author       = {Sebastian Eberhard and Stefan Hetzl},
 year         = {2015},
 title        = {Inductive theorem proving based on tree grammars},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {166},
 number       = {6},
 pages        = {665--700},
 doi          = {10.1016/j.apal.2015.01.002},
)
@article(Ebner2018generation,
 author       = {Gabriel Ebner and Stefan Hetzl and Alexander Leitsch and Giselle Reis and Daniel Weller},
 year         = {2018},
 title        = {On the generation of quantified lemmas},
 journal      = {Journal of Automated Reasoning},
 pages        = {1--32},
 doi          = {10.1007/s10817-018-9462-8},
)
@misc(GAPT2018User,
 author       = {Gabriel Ebner and Stefan Hetzl and Bernhard Mallinger and Giselle Reis and Martin Riener and Marielle Louise Rietdijk and Matthias Schlaipfer and Christoph Sp\"ork and Janos Tapolczai and Jannik Vierling and Daniel Weller and Simon Wolfsteiner and Sebastian Zivota},
 year         = {2018},
 title        = {{GAPT} user manual, version 2.10},
 url          = {https://logic.at/gapt/downloads/gapt-user-manual.pdf},
)
@inproceedings(Ebner2016System,
 author       = {Gabriel Ebner and Stefan Hetzl and Giselle Reis and Martin Riener and Simon Wolfsteiner and Sebastian Zivota},
 year         = {2016},
 title        = {System Description: {GAPT} 2.0},
 editor       = {Nicola Olivetti and Ashish Tiwari},
 booktitle    = {International Joint Conference on Automated Reasoning ({IJCAR})},
 series       = {Lecture Notes in Computer Science},
 volume       = {9706},
 publisher    = {Springer},
 pages        = {293--301},
 doi          = {10.1007/978-3-319-40229-1_20},
)
@article(Furstenberg1955infinitude,
 author       = {Harry Furstenberg},
 year         = {1955},
 title        = {On the infinitude of primes},
 journal      = {The American Mathematical Monthly},
 volume       = {62},
 number       = {5},
 pages        = {353},
 doi          = {10.2307/2307043},
)
@book(Furstenberg1981Recurrence,
 author       = {Harry Furstenberg},
 year         = {1981},
 title        = {Recurrence in ergodic theory and combinatorial number theory},
 publisher    = {Princeton University Press},
 doi          = {10.1515/9781400855162},
)
@article(Gentzen1935Untersuchungen,
 author       = {Gerhard Gentzen},
 year         = {1935},
 title        = {Untersuchungen {\"{u}}ber das logische Schlie{\ss}en I},
 journal      = {Mathematische Zeitschrift},
 volume       = {39},
 number       = {1},
 pages        = {176--210},
 doi          = {10.1007/BF01201353},
)
@article(Gentzen1936Widerspruchsfreiheit,
 author       = {Gerhard Gentzen},
 year         = {1936},
 title        = {Die Widerspruchsfreiheit der reinen Zahlentheorie},
 journal      = {Mathematische Annalen},
 volume       = {112},
 pages        = {493--565},
 doi          = {10.1007/BF01565428},
)
@article(Gerhardy2005Extracting,
 author       = {Philipp Gerhardy and Ulrich Kohlenbach},
 year         = {2005},
 title        = {Extracting Herbrand disjunctions by functional interpretation},
 journal      = {Archive for Mathematical Logic},
 volume       = {44},
 number       = {5},
 pages        = {633--644},
 doi          = {10.1007/s00153-005-0275-1},
)
@book(Girard1987Proof,
 author       = {Jean-Yves Girard},
 year         = {1987},
 title        = {Proof theory and logical complexity},
 volume       = {Vol. 1},
 publisher    = {Bibliopolis},
)
@book(Harper2016Practical,
 author       = {Robert Harper},
 year         = {2016},
 title        = {Practical foundations for programming languages},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781316576892},
)
@phdthesis(Herbrand1930Recherches,
 author       = {Jacques Herbrand},
 year         = {1930},
 title        = {Recherches sur la th{\'e}orie de la d{\'e}monstration},
 school       = {Universit\'{e} de Paris},
)
@inproceedings(Hetzl2012Applying,
 author       = {Stefan Hetzl},
 year         = {2012},
 title        = {Applying Tree Languages in Proof Theory},
 editor       = {Adrian-Horia Dediu and Mart{\'i}n-Vide, Carlos},
 booktitle    = {Language and Automata Theory and Applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {7183},
 publisher    = {Springer},
 pages        = {301--312},
 doi          = {10.1007/978-3-642-28332-1_26},
)
@inproceedings(Hetzl2014Introducing,
 author       = {Stefan Hetzl and Alexander Leitsch and Giselle Reis and Janos Tapolczai and Daniel Weller},
 year         = {2014},
 title        = {Introducing Quantified Cuts in Logic with Equality},
 editor       = {St{\'{e}}phane Demri and Deepak Kapur and Christoph Weidenbach},
 booktitle    = {7\textsuperscript{th} International Joint Conference on Automated Reasoning, {IJCAR}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8562},
 publisher    = {Springer},
 pages        = {240--254},
 doi          = {10.1007/978-3-319-08587-6_17},
)
@article(Hetzl2014Algorithmic,
 author       = {Stefan Hetzl and Alexander Leitsch and Giselle Reis and Daniel Weller},
 year         = {2014},
 title        = {Algorithmic introduction of quantified cuts},
 journal      = {Theoretical Computer Science},
 volume       = {549},
 pages        = {1--16},
 doi          = {10.1016/j.tcs.2014.05.018},
)
@article(Hetzl2011CERES,
 author       = {Stefan Hetzl and Alexander Leitsch and Daniel Weller},
 year         = {2011},
 title        = {{CERES} in higher-order logic},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {162},
 number       = {12},
 pages        = {1001--1034},
 doi          = {10.1016/j.apal.2011.06.005},
)
@inproceedings(Hetzl2012Towards,
 author       = {Stefan Hetzl and Alexander Leitsch and Daniel Weller},
 year         = {2012},
 title        = {{T}owards {A}lgorithmic {C}ut-{I}ntroduction},
 booktitle    = {Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18)},
 series       = {Lecture Notes in Computer Science},
 volume       = {7180},
 publisher    = {Springer},
 pages        = {228--242},
 doi          = {10.1007/978-3-642-28717-6_19},
)
@article(Hetzl2013Expansion,
 author       = {Stefan Hetzl and Daniel Weller},
 year         = {2013},
 title        = {Expansion Trees with Cut},
 journal      = {CoRR},
 volume       = {abs/1308.0428},
 url          = {https://arxiv.org/abs/1308.0428},
)
@book(Hilbert1939Grundlagen,
 author       = {David Hilbert and Paul Bernays},
 year         = {1939},
 title        = {Grundlagen der Mathematik II},
 publisher    = {Springer},
)
@article(Leitsch2018Extraction,
 author       = {Alexander Leitsch and Anela Lolic},
 year         = {2018},
 title        = {Extraction of Expansion Trees},
 journal      = {Journal of Automated Reasoning},
 pages        = {1--38},
 doi          = {10.1007/s10817-018-9453-9},
)
@article(Luckhardt1989Herbrand,
 author       = {Horst Luckhardt},
 year         = {1989},
 title        = {{Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken}},
 journal      = {Journal of Symbolic Logic},
 volume       = {54},
 number       = {1},
 pages        = {234--263},
 doi          = {10.2307/2275028},
)
@article(Miller1987Compact,
 author       = {Dale A. Miller},
 year         = {1987},
 title        = {A compact representation of proofs},
 journal      = {Studia Logica},
 volume       = {46},
 number       = {4},
 pages        = {347--370},
 doi          = {10.1007/BF00370646},
)
@inproceedings(Parigot1992Lambda,
 author       = {Michel Parigot},
 year         = {1992},
 title        = {$\lambda\mu $-Calculus: An Algorithmic Interpretation of Classical Natural Deduction},
 editor       = {Andrei Voronkov},
 booktitle    = {Logic for Programming, Artificial Intelligence and Reasoning (LPAR)},
 series       = {Lecture Notes in Computer Science},
 volume       = {624},
 publisher    = {Springer},
 pages        = {190--201},
 doi          = {10.1007/BFb0013061},
)
@inproceedings(Pfenning1995Structural,
 author       = {Frank Pfenning},
 year         = {1995},
 title        = {Structural Cut Elimination},
 booktitle    = {Logic in Computer Science},
 publisher    = {{IEEE} Computer Society},
 pages        = {156--166},
 doi          = {10.1109/LICS.1995.523253},
)
@book(Takeuti1987Proof,
 author       = {Gaisi Takeuti},
 year         = {1987},
 title        = {Proof theory},
 edition      = {second},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {81},
 publisher    = {North-Holland Publishing Co.},
 address      = {Amsterdam},
)
@article(Urban2001Strong,
 author       = {Christian Urban and Gavin M. Bierman},
 year         = {2001},
 title        = {Strong Normalisation of Cut-Elimination in Classical Logic},
 journal      = {Fundamenta informaticae},
 volume       = {45},
 number       = {1-2},
 pages        = {123--155},
 doi          = {10.1007/3-540-48959-2_26},
)