Document Open Access Logo

Tree Grammars for the Elimination of Non-prenex Cuts

Authors Stefan Hetzl, Sebastian Zivota

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2015.110.pdf
  • Filesize: 461 kB
  • 18 pages

Document Identifiers

Subject Classification

Keywords
  • proof theory
  • cut-elimination
  • Herbrand's theorem
  • tree grammars

Metrics

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

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 with prenex Pi_1-cuts in classical first-order logic corresponds to computing the language of a particular type of tree grammars. The present paper extends this connection to arbitrary (i.e. non-prenex) cuts without quantifier alternations. The key to treating non-prenex cuts lies in using a new class of tree grammars, constraint grammars, which describe the relationship of the applicability of its productions by a propositional formula.

Cite As Get BibTex

Stefan Hetzl and Sebastian Zivota. Tree Grammars for the Elimination of Non-prenex Cuts. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 110-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.110

Author Details

Stefan Hetzl
Sebastian Zivota

References

  1. Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh. Herbrand disjunctions, cut elimination and context-free tree grammars. to appear at Typed Lambda Calculi and Applications (TLCA) 2015. Google Scholar
  2. 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
  3. Sebastian Eberhard and Stefan Hetzl. Compressibility of finite languages by grammars. to appear at Descriptional Complexity of Formal Systems (DCFS) 2015, preprint available at URL: http://www.logic.at/people/hetzl/research/.
  4. Sebastian Eberhard and Stefan Hetzl. Inductive theorem proving based on tree grammars. Annals of Pure and Applied Logic, 166(6):665-700, 2015. Google Scholar
  5. Philipp Gerhardy and Ulrich Kohlenbach. Extracting Herbrand Disjunctions by Functional Interpretation. Archive for Mathematical Logic, 44:633-644, 2005. Google Scholar
  6. Willem Heijltjes. Classical proof forestry. Annals of Pure and Applied Logic, 161(11):1346-1366, 2010. Google Scholar
  7. Jacques Herbrand. Recherches sur la théorie de la démonstration. PhD thesis, Université de Paris, 1930. Google Scholar
  8. 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
  9. 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
  10. Stefan Hetzl, Alexander Leitsch, Giselle Reis, and Daniel Weller. Algorithmic introduction of quantified cuts. Theoretical Computer Science, 549:1-16, 2014. Google Scholar
  11. 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
  12. 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
  13. Stefan Hetzl and Daniel Weller. Expansion trees with cut. preprint, available at http://arxiv.org/abs/1308.0428, 2013.
  14. David Hilbert and Paul Bernays. Grundlagen der Mathematik II. Springer, 1939. Google Scholar
  15. Markus Lohrey. Algorithmics on SLP-compressed strings: A survey. Groups Complexity Cryptology, 4(2):241-299, 2012. Google Scholar
  16. Richard McKinley. Proof nets for Herbrand’s Theorem. ACM Transactions on Computational Logic, 14(1):5:1-5:31, 2013. Google Scholar
  17. Dale A. Miller. A compact representation of proofs. Studia Logica, 46(4):347-370, 1987. Google Scholar
  18. 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
  19. Pavel Pudlák. The Lengths of Proofs. In Sam Buss, editor, Handbook of Proof Theory, pages 547-637. Elsevier, 1998. Google Scholar
  20. Richard Statman. Lower bounds on Herbrand’s theorem. Proceedings of the American Mathematical Society, 75:104-107, 1979. Google Scholar
  21. Sebastian Zivota. Cuts Without Quantifier Alternations and Their Effect on Expansion Trees. Master’s thesis, Vienna University of Technology, 2014. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact