Record link: 
http://hdl.handle.net/20.500.12708/41408
-
Title: 
Tree Grammars for the Elimination of Non-prenex Cuts
en
Citation: 
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
-
Publisher DOI: 
10.4230/LIPIcs.CSL.2015.110
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Hetzl, Stefan 
Zivota, Sebastian 
-
Organisational Unit: 
E104-05 - Forschungsbereich Kombinatorik und Algorithmen 
E104-02 - Forschungsbereich Computational Logic 
-
Published in: 
24th EACSL Annual Conference on Computer Science Logic - CLS 2015 
-
ISBN: 
978-3-939897-90-3
-
Volume: 
41
-
Date (published): 
2015
-
Event name: 
CSL 2015 
-
Event date: 
7-Sep-2015 - 10-Sep-2015
-
Event place: 
Berlin, Germany
-
Number of Pages: 
18
-
Publisher: 
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%
-
Science Branch: 
Mathematik
-
Appears in Collections:
Conference Paper

Show full item record

Google ScholarTM

Check