Beiträge in Tagungsbänden:
B. Afshari, S. Hetzl, G. Leigh:
"Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars";
in: "13th International Conference on Typed Lambda Calculi and Applications - TLCA 2015",
38;
herausgegeben von: Thorsten Altenkirch;
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
Dagstuhl, Deutschland,
2015,
ISBN: 978-3-939897-87-3,
S. 1
- 16.
Kurzfassung englisch:
Recently a new connection between proof theory and formal language theory was introduced. It was shown that the operation of cut elimination for proofs in first-order predicate logic involving Pi_1-cuts corresponds to computing the language of a particular class of regular tree grammars. The present paper expands this connection to the level of Pi_2-cuts. Given a proof pi of a Sigma_1 formula with cuts only on Pi_2 formulæ, we show there is associated to pi a natural context-free tree grammar whose language is finite and yields a Herbrand disjunction for pi.
Schlagworte:
Classical logic; Context-free grammars; Cut elimination; First-order logic; Herbrand´s theorem; Proof theory
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.1
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.