Herbrand Expansion: A Bridge between Mathematical Logic and Theoretical Computer Science

Herbrand s theorem belongs to the greatest results in logic of the 20th century and had a major impact on proof theory and automated deduction. Recently a new connection between proof theory and formal language theory was introduced by Stefan Hetzl. In this paper, we explain how Herbrand expansion works as a bridge between proof theory in mathematical logic (in one hand) and formal language theory in theoretical computer science (in the other hand). We show that the operation of cut-elimination for special proofs in first-order predicate logic corresponds to computing the language of a particular class of regular tree grammar.