To the top

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

Tell a friend about this page
Print version

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

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


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

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?