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 (6)

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

This page was built for publication: Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars