Proofs as Tree Languages
Stefan Hetzl · HAL (Le Centre pour la Communication Scientifique Directe) · 2011
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.