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