Show simple item record

dc.contributor.authorAfshari, Bahareh
dc.contributor.authorHetzl, Stefan
dc.contributor.authorLeigh, Graham E.
dc.date.accessioned2018-02-19T10:16:48Z
dc.date.available2018-02-19T10:16:48Z
dc.date.issued2018-02-19
dc.identifier.urihttp://publications.mfo.de/handle/mfo/1333
dc.descriptionResearch in Pairs 2016en_US
dc.description.abstractWe 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.isoen_USen_US
dc.publisherMathematisches Forschungsinstitut Oberwolfachen_US
dc.relation.ispartofseriesOberwolfach Preprints;2018,01
dc.titleHerbrand’s Theorem as Higher Order Recursionen_US
dc.typePreprinten_US
dc.identifier.doi10.14760/OWP-2018-01
local.scientificprogramResearch in Pairs 2016en_US
local.series.idOWP-2018-01
dc.identifier.urnurn:nbn:de:101:1-2018032020424
dc.identifier.ppn1654581453


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record