Herbrand's theorem as higher order recursion

DOI10.1016/j.apal.2020.102792zbMath1464.03085OpenAlexW2800852260MaRDI QIDQ1987218

Bahareh Afshari, Stefan Hetzl, Graham E. Leigh

Publication date: 14 April 2020

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2020.102792

zbMATH Keywords

cut eliminationHerbrand's theoremclassical sequent calculuscomputational contenthigher-order recursion schemes

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Structure of proofs (03F07)

Related Items

On extracting variable Herbrand disjunctions ⋮ On the generation of quantified lemmas ⋮ Unnamed Item ⋮ Exact bounds for acyclic higher-order recursion schemes

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algorithmic introduction of quantified cuts
• Classical proof forestry
• The epsilon calculus and Herbrand complexity
• A quantitative version of Kirk's fixed point theorem for asymptotic contractions
• A compact representation of proofs
• The problem of \(\Pi_{2}\)-cut-introduction
• Untersuchungen über das logische Schliessen. II
• A herbrandized functional interpretation of classical first-order logic
• Extracting Herbrand disjunctions by functional interpretation
• Exact bounds for lengths of reductions in typed λ-calculus
• Exploring the Computational Content of the Infinite Pigeonhole Principle
• Applying Tree Languages in Proof Theory
• Towards Algorithmic Cut-Introduction
• Proof Nets for Herbrand’s Theorem
• On the non-confluence of cut-elimination
• Introducing Quantified Cuts in Logic with Equality
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Shoenfield is Gödel after Krivine
• A semantics of evidence for classical arithmetic
• Recursion Schemes, Collapsible Pushdown Automata and Higher-Order Model Checking
• Herbrand Confluence for First-Order Proofs with Π₂-Cuts
• Expansion trees with cut
• Types and higher-order recursion schemes for verification of higher-order programs
• Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars
• Cut Elimination In Situ
• Verifying higher-order functional programs with pattern-matching algebraic data types
• Logic for Programming, Artificial Intelligence, and Reasoning
• Cut-elimination and redundancy-elimination by resolution