<div class="csl-bib-body">
<div class="csl-entry">Hetzl, S., & Zivota, S. (2015). Tree Grammars for the Elimination of Non-prenex Cuts. In S. Kreutzer (Ed.), <i>24th EACSL Annual Conference on Computer Science Logic - CLS 2015</i> (pp. 110–127). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CSL.2015.110</div>
</div>
-
dc.identifier.isbn
978-3-939897-90-3
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/41408
-
dc.description.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.
en
dc.language.iso
en
-
dc.publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
-
dc.relation.ispartofseries
Leibniz International Proceedings in Informatics (LIPIcs)
-
dc.title
Tree Grammars for the Elimination of Non-prenex Cuts
