Proofs as Tree Languages
Overview & Synopsis
In this work a new connection between proof theory and formal language theory is established. Cut-elimination in a class of first-order proofs is characterised by a class of tree languages in the following sense: the proof with cuts corresponds to a formal grammar, the cut-free proof to the language of the grammar and the process of cut-elimination to the computation of the language from the grammar. It is shown how to read off a grammar from a proof and vice versa how to construct a proof from a grammar such that this correspondence holds.
Indexed from repository: HAL Open Science
(
hal.science)
Keyboard Shortcuts:
← / → for pages • + / - for zoom • 0 to fit width
Powered by Mozilla PDF.js v3.11
Document Information
| Document Title | Proofs as Tree Languages |
|---|---|
| Author / Organization | Stefan Hetzl |
| Subject & Discipline | Multidisciplinary Academic Open Research |
| Categories | Science & Mathematics |
| Publication Year | 2011 |
| License / Rights | Open Access / Creative Commons |
| Resource Verification | Listed PDF (Verification Pending) |
| Original Host Website |
HAL Open Science
(hal.science)
|
| File Format | application/pdf (Portable Document Format) |
| Language | EN |
| Catalog ID | DOC-243549 |
| Original Source Link | Visit Source Page on hal.science » |