Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

Herbrand disjunctions, cu… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Herbrand disjunctions, cut elimination and context-free tree grammars

Paper i proceeding
Författare Bahareh Afshari
Stefan Hetzl
Graham E. Leigh
Publicerad i Leibniz International Proceedings in Informatics, LIPIcs
ISSN 1868-8969
Publiceringsår 2015
Publicerad vid
Språk en
Ämnesord Classical logic , Context-free grammars , Cut elimination , First-order logic , Herbrand's theorem , Proof theory
Ämneskategorier Teoretisk datalogi, Matematisk logik

Sammanfattning

Recently a new connection between proof theory and formal language theory was introduced. It was shown that the operation of cut elimination for proofs in first-order predicate logic involving Π1-cuts corresponds to computing the language of a particular class of regular tree grammars. The present paper expands this connection to the level of Π2-cuts. Given a proof π of a ∑1 formulæ with cuts only on Π2 formula, we show there is associated to π a natural context-free tree grammar whose language is finite and yields a Herbrand disjunction for π. © Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?