Hetzl, S., & Zivota, S. (2015). Tree Grammars for the Elimination of Non-prenex Cuts. In S. Kreutzer (Ed.), 24th EACSL Annual Conference on Computer Science Logic - CLS 2015 (pp. 110–127). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CSL.2015.110
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Deutschland
-
Publisher:
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl
-
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
Research Areas:
außerhalb der gesamtuniversitären Forschungsschwerpunkte: 100%