Premium
Herbrand's theorem revisited
Author(s) -
Afshari Bahareh,
Hetzl Stefan,
Leigh Graham E.
Publication year - 2016
Publication title -
pamm
Language(s) - English
Resource type - Journals
ISSN - 1617-7061
DOI - 10.1002/pamm.201610441
Subject(s) - mathematical proof , proof theory , structural proof theory , proof complexity , analytic proof , equivalence (formal languages) , mathematics , recursion (computer science) , automated theorem proving , formal proof , connection (principal bundle) , discrete mathematics , algebra over a field , computer science , pure mathematics , algorithm , geometry
We present recent results on the deepening connection between proof theory and formal language theory. To each first‐order proof with prenex cuts of complexity at most Π n /Σ n , we associate a typed (non‐deterministic) tree grammar of order n (equivalently, an order n recursion scheme) that abstracts the computation of Herbrand sets obtained through Gentzen‐style cut elimination. Apart from offering a means to compute Herbrand expansions directly from proofs with cuts, these grammars provide a structural counterpart to Herbrand's theorem that opens the door to tackling a number of questions in proof theory such as proof equivalence, proof compression and proof complexity. (© 2016 Wiley‐VCH Verlag GmbH & Co. KGaA, Weinheim)