Herbrand Confluence for First-Order Proofs with Π2-Cuts

DOI10.1515/9781501502620-003zbMath1433.03133OpenAlexW2485473430MaRDI QIDQ5221602

Bahareh Afshari, Stefan Hetzl, Graham E. Leigh

Publication date: 2 April 2020

Published in: Concepts of Proof in Mathematics, Philosophy, and Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1515/9781501502620-003

zbMATH Keywords

first-order logiccut eliminationHerbrand's theoremformal language theory

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42) Structure of proofs (03F07)

Related Items

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