References

  1. Bahareh Afshari, Stefan Hetzl & Graham Leigh (2018): Herbrand's Theorem as Higher Order Recursion, doi:10.14760/OWP-2018-01.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. David Cerna & Anela Lolic (2018): System Description: GAPT for schematic proofs. RISC Report Series. Available at http://www.risc.jku.at/publications/download/risc_5591/schematicGapt.pdf.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. Harry Furstenberg (1955): On the infinitude of primes. The American Mathematical Monthly 62(5), pp. 353, doi:10.2307/2307043.
  14. Harry Furstenberg (1981): Recurrence in ergodic theory and combinatorial number theory. Princeton University Press, doi:10.1515/9781400855162.
  15. Gerhard Gentzen (1935): Untersuchungen über das logische Schließen I. Mathematische Zeitschrift 39(1), pp. 176–210, doi:10.1007/BF01201353.
  16. Gerhard Gentzen (1936): Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen 112, pp. 493–565, doi:10.1007/BF01565428.
  17. 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.
  18. Jean-Yves Girard (1987): Proof theory and logical complexity Vol. 1. Bibliopolis.
  19. Robert Harper (2016): Practical foundations for programming languages. Cambridge University Press, doi:10.1017/CBO9781316576892.
  20. Jacques Herbrand (1930): Recherches sur la théorie de la démonstration. Université de Paris.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. 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.
  26. Stefan Hetzl & Daniel Weller (2013): Expansion Trees with Cut. CoRR abs/1308.0428. Available at https://arxiv.org/abs/1308.0428.
  27. David Hilbert & Paul Bernays (1939): Grundlagen der Mathematik II. Springer.
  28. Alexander Leitsch & Anela Lolic (2018): Extraction of Expansion Trees. Journal of Automated Reasoning, pp. 1–38, doi:10.1007/s10817-018-9453-9.
  29. 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.
  30. Dale A. Miller (1987): A compact representation of proofs. Studia Logica 46(4), pp. 347–370, doi:10.1007/BF00370646.
  31. 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.
  32. Frank Pfenning (1995): Structural Cut Elimination. In: Logic in Computer Science. IEEE Computer Society, pp. 156–166, doi:10.1109/LICS.1995.523253.
  33. Gaisi Takeuti (1987): Proof theory, second edition, Studies in Logic and the Foundations of Mathematics 81. North-Holland Publishing Co., Amsterdam.
  34. 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.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org