Document Open Access Logo

Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars

Authors Bahareh Afshari, Stefan Hetzl, Graham E. Leigh

PDF
Thumbnail PDF

File

LIPIcs.TLCA.2015.1.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Bahareh Afshari
Stefan Hetzl
Graham E. Leigh

Cite As Get BibTex

Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh. Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.1

Abstract

Recently a new connection between proof theory and formal language theory was introduced. It was shown that the operation of cut elimination for proofs in first-order predicate logic involving Pi_1-cuts corresponds to computing the language of a particular class of regular tree grammars. The present paper expands this connection to the level of Pi_2-cuts. Given a proof pi of a Sigma_1 formula with cuts only on Pi_2 formulæ, we show there is associated to pi a natural context-free tree grammar whose language is finite and yields a Herbrand disjunction for pi.

Subject Classification

Keywords
  • Classical logic
  • Context-free grammars
  • Cut elimination
  • First-order logic
  • Herbrand's theorem
  • Proof theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh. On Herbrand confluence for first-order logic. Submitted, 2015. Google Scholar
  2. Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, and Hendrik Spohr. Cut-Elimination: Experiments with CERES. In Franz Baader and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) 2004, volume 3452 of Lecture Notes in Computer Science, pages 481-495. Springer, 2005. Google Scholar
  3. Franco Barbanera, Stefano Berardi, and Massimo Schivalocchi. “Classical” programming-with-proofs in λ^Sym_PA: An analysis of non-confluence. In Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software, volume 1281 of Lecture Notes in Computer Science, pages 365-390. Springer Berlin Heidelberg, 1997. Google Scholar
  4. Hendrik Pieter Barendregt. The Lambda Calculus, volume 103 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1984. Google Scholar
  5. Samuel R. Buss. On Herbrand’s Theorem. In Logic and Computational Complexity, volume 960 of Lecture Notes in Computer Science, pages 195-209. Springer, 1995. Google Scholar
  6. Thierry Coquand. A semantics of evidence for classical arithmetic. Journal of Symbolic Logic, 60(1):325-337, 1995. Google Scholar
  7. Sebastian Eberhard and Stefan Hetzl. Compressibility of finite languages by grammars. preprint, available at http://www.logic.at/people/hetzl/research/, 2015.
  8. Sebastian Eberhard and Stefan Hetzl. Inductive theorem proving based on tree grammars. to appear in the Annals of Pure and Applied Logic, preprint available at http://www.logic.at/people/hetzl/research/, 2015.
  9. Philipp Gerhardy and Ulrich Kohlenbach. Extracting Herbrand Disjunctions by Functional Interpretation. Archive for Mathematical Logic, 44:633-644, 2005. Google Scholar
  10. Willem Heijltjes. Classical proof forestry. Annals of Pure and Applied Logic, 161(11):1346-1366, 2010. Google Scholar
  11. Hugo Herbelin. Séquents qu'on calcule. PhD thesis, Université Paris 7, 1995. Google Scholar
  12. Jacques Herbrand. Recherches sur la théorie de la démonstration. PhD thesis, Université de Paris, 1930. Google Scholar
  13. Stefan Hetzl. On the form of witness terms. Archive for Mathematical Logic, 49(5):529-554, 2010. Google Scholar
  14. Stefan Hetzl. Applying Tree Languages in Proof Theory. In Adrian-Horia Dediu and Carlos Martín-Vide, editors, Language and Automata Theory and Applications (LATA) 2012, volume 7183 of Lecture Notes in Computer Science, pages 301-312. Springer, 2012. Google Scholar
  15. Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai, and Daniel Weller. Introducing Quantified Cuts in Logic with Equality. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, Automated Reasoning - 7th International Joint Conference, IJCAR, volume 8562 of Lecture Notes in Computer Science, pages 240-254. Springer, 2014. Google Scholar
  16. Stefan Hetzl, Alexander Leitsch, Giselle Reis, and Daniel Weller. Algorithmic introduction of quantified cuts. Theoretical Computer Science, 549:1-16, 2014. Google Scholar
  17. Stefan Hetzl, Alexander Leitsch, and Daniel Weller. Towards Algorithmic Cut-Introduction. In Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), volume 7180 of Lecture Notes in Computer Science, pages 228-242. Springer, 2012. Google Scholar
  18. Stefan Hetzl and Lutz Straßburger. Herbrand-Confluence for Cut-Elimination in Classical First-Order Logic. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL) 2012, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs), pages 320-334. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2012. Google Scholar
  19. Stefan Hetzl and Daniel Weller. Expansion trees with cut. preprint, available at http://arxiv.org/abs/1308.0428, 2013.
  20. David Hilbert and Paul Bernays. Grundlagen der Mathematik II. Springer, 1939. Google Scholar
  21. Florent Jacquemard, Francis Klay, and Camille Vacher. Rigid tree automata. In Adrian Horia Dediu, Armand-Mihai Ionescu, and Carlos Martín-Vide, editors, Language and Automata Theory and Applications (LATA) 2009, volume 5457 of Lecture Notes in Computer Science, pages 446-457. Springer, 2009. Google Scholar
  22. Florent Jacquemard, Francis Klay, and Camille Vacher. Rigid tree automata and applications. Information and Computation, 209:486-512, 2011. Google Scholar
  23. Markus Lohrey. Algorithmics on SLP-compressed strings: A survey. Groups Complexity Cryptology, 4(2):241-299, 2012. Google Scholar
  24. Richard McKinley. Proof nets for Herbrand’s Theorem. ACM Transactions on Computational Logic, 14(1):5:1-5:31, 2013. Google Scholar
  25. Dale Miller. A Compact Representation of Proofs. Studia Logica, 46(4):347-370, 1987. Google Scholar
  26. V.P. Orevkov. Lower bounds for increasing complexity of derivations after cut elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta, 88:137-161, 1979. Google Scholar
  27. Pavel Pudlák. The Lengths of Proofs. In Sam Buss, editor, Handbook of Proof Theory, pages 547-637. Elsevier, 1998. Google Scholar
  28. Diana Ratiu and Trifon Trifonov. Exploring the Computational Content of the Infinite Pigeonhole Principle. Journal of Logic and Computation, 22(2):329-350, 2012. Google Scholar
  29. Monika Seisenberger. On the Constructive Content of Proofs. PhD thesis, Ludwig-Maximilians-Universität München, 2003. Google Scholar
  30. Richard Statman. Lower bounds on Herbrand’s theorem. Proceedings of the American Mathematical Society, 75:104-107, 1979. Google Scholar
  31. G. Takeuti. Proof Theory. Dover Books on Mathematics Series. Dover Publications, Incorporated, 2013. Google Scholar
  32. Anne S. Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2000. Google Scholar
  33. Christian Urban. Classical Logic and Computation. PhD thesis, University of Cambridge, 2000. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact