dc.contributor.author Afshari, Bahareh dc.contributor.author Hetzl, Stefan dc.contributor.author Leigh, Graham E. dc.date.accessioned 2018-02-19T10:16:48Z dc.date.available 2018-02-19T10:16:48Z dc.date.issued 2018-02-19 dc.identifier.uri http://publications.mfo.de/handle/mfo/1333 dc.description Research in Pairs 2016 en_US dc.description.abstract We provide a means to compute Herbrand disjunctions directly from sequent calculus proofs with cuts. Our approach associates to a first-order classical proof $\pi \vdash \exists v F$, where $F$ is quantifier free, an acyclic higher order recursion scheme $\mathscr H$ whose language is finite and yields a Herbrand disjunction for $\exists v F$. More generally, we show that the language of $\mathscr H$ contains the Herbrand disjunction implicit in any cut-free proof obtained from $\pi$ via a sequence of Gentzen-style cut reductions that always reduce the weak side of a cut before the strong side. en_US dc.language.iso en_US en_US dc.publisher Mathematisches Forschungsinstitut Oberwolfach en_US dc.relation.ispartofseries Oberwolfach Preprints;2018,01 dc.title Herbrand’s Theorem as Higher Order Recursion en_US dc.type Preprint en_US dc.identifier.doi 10.14760/OWP-2018-01 local.scientificprogram Research in Pairs 2016 en_US local.series.id OWP-2018-01 dc.identifier.urn urn:nbn:de:101:1-2018032020424 dc.identifier.ppn 1654581453
﻿