Herbrand's theorem as higher order recursion
From MaRDI portal
Publication:1987218
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
cut eliminationHerbrand's theoremclassical sequent calculuscomputational contenthigher-order recursion schemes
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 Π2-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
