Contributions to Proceedings:
S. Hetzl, S. Zivota:
"Tree Grammars for the Elimination of Non-prenex Cuts";
in: "24th EACSL Annual Conference on Computer Science Logic - CLS 2015",
41;
issued by: Stephan Kreutzer;
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
Dagstuhl, Deutschland,
2015,
ISBN: 978-3-939897-90-3,
110
- 127.
English 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.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.4230/LIPIcs.CSL.2015.110
Created from the Publication Database of the Vienna University of Technology.