@inproceedings(AHL15,
 author       = {Bahareh Afshari and Stefan Hetzl and Graham~E. Leigh},
 year         = {2015},
 title        = {{Herbrand disjunctions, cut elimination and context-free tree grammars}},
 editor       = {Thorsten Altenkirch},
 booktitle    = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {38},
 publisher    = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
 address      = {Dagstuhl, Germany},
 pages        = {1--16},
 doi          = {10.4230/LIPIcs.TLCA.2015.1},
)
@incollection(AHL16,
 author       = {Bahareh Afshari and Stefan Hetzl and Graham~E. Leigh},
 year         = {2016},
 title        = {Herbrand confluence for first-order proofs with $\Pi_2$-cuts},
 editor       = {Dieter Probst and Peter Schuster},
 booktitle    = {Concepts of Proof in Mathematics, Philosophy, and Computer Science},
 series       = {Ontos Mathematical Logic},
 publisher    = {De Gruyter},
 address      = {Berlin, Boston},
 note         = {\href{http://www.degruyter.com/view/product/456623}{isbn: 978-1-5015-0262-0}. Preprint avaiable at \url{http://dmg.tuwien.ac.at/afshari/publications.html}},
)
@incollection(Bus95,
 author       = {Samuel~R. Buss},
 year         = {1995},
 title        = {{O}n {H}erbrand's theorem},
 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},
)
@unpublished(EberhardXXCompressibility,
 author       = {Sebastian Eberhard and Stefan Hetzl},
 title        = {{On the compressibility of finite languages and formal proofs}},
 note         = {In preparation, preprint available at \url{http://www.logic.at/people/hetzl/research/}},
)
@inproceedings(Eberhard15Compressibility,
 author       = {Sebastian Eberhard and Stefan Hetzl},
 year         = {2015},
 title        = {{Compressibility of finite languages by grammars}},
 editor       = {Jeffrey Shallit and Alexander Okhotin},
 booktitle    = {Descriptional Complexity of Formal Systems (DCFS) 2015},
 series       = {Lecture Notes in Computer Science},
 volume       = {9118},
 publisher    = {Springer},
 pages        = {93--104},
 doi          = {10.1007/978-3-319-19225-3\_8},
)
@article(EH15Inductive,
 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(GK05,
 author       = {Philipp Gerhardy and Ulrich Kohlenbach},
 year         = {2005},
 title        = {Extracting {H}erbrand disjunctions by functional interpretation},
 journal      = {Archive for Mathematical Logic},
 volume       = {44},
 pages        = {633--644},
 doi          = {10.1007/s00153-005-0275-1},
)
@article(Hei10,
 author       = {Willem Heijltjes},
 year         = {2010},
 title        = {{C}lassical proof forestry},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {161},
 number       = {11},
 pages        = {1346--1366},
 doi          = {10.1016/j.apal.2010.04.006},
)
@phdthesis(Her30,
 author       = {Jacques Herbrand},
 year         = {1930},
 title        = {Recherches sur la th{\'e}orie de la d{\'e}monstration},
 school       = {Universit\'{e} de Paris},
)
@inproceedings(Het12,
 author       = {Stefan Hetzl},
 year         = {2012},
 title        = {{A}pplying tree languages in proof theory},
 editor       = {Adrian-Horia Dediu and Mart{\'i}n-Vide, Carlos},
 booktitle    = {Language and Automata Theory and Applications (LATA) 2012},
 series       = {Lecture Notes in Computer Science},
 volume       = {7183},
 publisher    = {Springer},
 pages        = {301--312},
 doi          = {10.1007/978-3-642-28332-1\_26},
)
@inproceedings(HLRTW14,
 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    = {Automated Reasoning - 7th International Joint Conference, {IJCAR}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8562},
 publisher    = {Springer},
 pages        = {240--254},
 doi          = {10.1007/978-3-319-08587-6\_17},
)
@article(HLRW14,
 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},
)
@inproceedings(HLW12,
 author       = {Stefan Hetzl and Alexander Leitsch and Daniel Weller},
 year         = {2012},
 title        = {{T}owards algorithmic cut-introduction},
 editor       = {Andrei Bj{\o}rner, Nikolaj \&~Voronkov},
 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},
)
@unpublished(HW13,
 author       = {Stefan Hetzl and Daniel Weller},
 year         = {2013},
 title        = {Expansion trees with cut},
 note         = {Preprint available at \url{http://arxiv.org/abs/1308.0428}},
)
@book(HB39,
 author       = {David Hilbert and Paul Bernays},
 year         = {1939},
 title        = {{G}rundlagen der {M}athematik {II}},
 publisher    = {Springer},
)
@article(McK13,
 author       = {Richard McKinley},
 year         = {2013},
 title        = {{Proof nets for Herbrand's theorem}},
 journal      = {ACM Transactions on Computational Logic},
 volume       = {14},
 number       = {1},
 pages        = {5:1--5:31},
 doi          = {10.1145/2422085.2422090},
)
@article(Mil87,
 author       = {Dale Miller},
 year         = {1987},
 title        = {A compact representation of proofs},
 journal      = {Studia Logica},
 volume       = {46},
 number       = {4},
 pages        = {347--370},
 doi          = {10.1007/BF00370646},
)