Tree Grammars for the Elimination of Non-prenex Cuts

Authors Stefan Hetzl, Sebastian Zivota

Thumbnail PDF


  • Filesize: 461 kB
  • 18 pages

Document Identifiers

Author Details

Stefan Hetzl
Sebastian Zivota

Cite AsGet 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)


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.
  • proof theory
  • cut-elimination
  • Herbrand's theorem
  • tree grammars


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


  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:
  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, 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