Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars

DOI10.4230/LIPIcs.TLCA.2015.1zbMath1366.03235OpenAlexW2294622924MaRDI QIDQ5277826

Stefan Hetzl, Bahareh Afshari, Graham E. Leigh

Publication date: 12 July 2017

Full work available at URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.1

zbMATH Keywords

first-order logiccut eliminationcontext-free grammarsproof theoryclassical logicHerbrand's theorem

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42)

Related Items

Unnamed Item, The problem of \(\Pi_{2}\)-cut-introduction, On the Herbrand content of LK, On the generation of quantified lemmas, On the compressibility of finite languages and formal proofs, Herbrand's theorem as higher order recursion