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

On the Herbrand content of LK

Conference paper
Authors Bahareh Afshari
Stefan Hetzl
Graham E. Leigh
Published in Proceedings Sixth International Workshop on Classical Logic and Computation (CL&C16). Porto, Portugal , 23th June 2016
ISSN 2075-2180
Publication year 2016
Published at
Language en
Subject categories Mathematical logic, Theoretical computer science

Abstract

We present a structural representation of the Herbrand content of LK-proofs with cuts of complexity prenex Sigma-2/Pi-2. The representation takes the form of a typed non-deterministic tree grammar of order 2 which generates a finite language of first-order terms that appear in the Herbrand expansions obtained through cut-elimination. In particular, for every Gentzen-style reduction between LK-proofs we study the induced grammars and classify the cases in which language equality and inclusion hold.

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?