Zur Kurzanzeige

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.rights.licenseDieses Dokument darf im Rahmen von § 53 UrhG zum eigenen Gebrauch kostenfrei heruntergeladen, gelesen, gespeichert und ausgedruckt, aber nicht im Internet bereitgestellt oder an Außenstehende weitergegeben werden.de
dc.rights.licenseThis document may be downloaded, read, stored and printed for your own use within the limits of § 53 UrhG but it may not be distributed via the internet or passed on to external parties.en
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


Dateien zu dieser Ressource

Thumbnail

Das Dokument erscheint in:

Zur Kurzanzeige