文章基本信息

标题：Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars
本地全文：下载
作者：Bahareh Afshari ; Stefan Hetzl ; Graham E. Leigh 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：38
页码：1-16
DOI：10.4230/LIPIcs.TLCA.2015.1
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Classical logic; Context-free grammars; Cut elimination; First-order logic; Herbrand's theorem; Proof theory