Till startsida
Sitemap
To content Read more about how we use cookies on gu.se

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 Mathematical logic, Theoretical computer science

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 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
Share:

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?