To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Herbrand disjunctions, cu… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Herbrand disjunctions, cut elimination and context-free tree grammars

Conference paper
Authors Bahareh Afshari
Stefan Hetzl
Graham E. Leigh
Published in Leibniz International Proceedings in Informatics, LIPIcs
ISSN 1868-8969
Publication year 2015
Published at
Language en
Keywords Classical logic , Context-free grammars , Cut elimination , First-order logic , Herbrand's theorem , Proof theory
Subject categories Theoretical computer science, Mathematical logic


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 Π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 Π2-cuts. Given a proof π of a ∑1 formulæ with cuts only on Π2 formula, we show there is associated to π a natural context-free tree grammar whose language is finite and yields a Herbrand disjunction for π. © Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?