On the Herbrand content of LK

zbMath1482.03014arXiv1606.06384MaRDI QIDQ5015361

Bahareh Afshari, Stefan Hetzl, Graham E. Leigh

Publication date: 7 December 2021

Full work available at URL: https://arxiv.org/abs/1606.06384

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Structure of proofs (03F07)

Related Items (1)

On the generation of quantified lemmas

Cites Work

• Unnamed Item
• Algorithmic introduction of quantified cuts
• Classical proof forestry
• A compact representation of proofs
• On the compressibility of finite languages and formal proofs
• Inductive theorem proving based on tree grammars
• Extracting Herbrand disjunctions by functional interpretation
• Applying Tree Languages in Proof Theory
• Towards Algorithmic Cut-Introduction
• Proof Nets for Herbrand’s Theorem
• Introducing Quantified Cuts in Logic with Equality
• Herbrand Confluence for First-Order Proofs with Π₂-Cuts
• Expansion trees with cut
• Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars
• Compressibility of Finite Languages by Grammars
• On Herbrand's theorem

This page was built for publication: On the Herbrand content of LK