Expansion trees with cut
From MaRDI portal
Publication:5236547
DOI10.1017/S0960129519000069zbMath1456.03085arXiv1802.08076OpenAlexW3097995181WikidataQ127126656 ScholiaQ127126656MaRDI QIDQ5236547
Federico Aschieri, Daniel Weller, Stefan Hetzl
Publication date: 9 October 2019
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1802.08076
Related Items (5)
On the Herbrand content of LK ⋮ Unnamed Item ⋮ Extraction of expansion trees ⋮ Herbrand's theorem as higher order recursion ⋮ Unnamed Item
Cites Work
- Unnamed Item
- Unnamed Item
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
- Linear logic
- Classical proof forestry
- The epsilon calculus and Herbrand complexity
- A compact representation of proofs
- Cut normal forms and proof complexity
- The computational content of arithmetical proofs
- System Description: GAPT 2.0
- Exploring the Computational Content of the Infinite Pigeonhole Principle
- The duality of computation
- Proof Nets for Herbrand’s Theorem
- On the non-confluence of cut-elimination
- A new deconstructive logic: linear logic
- Herbrand-Confluence for Cut Elimination in Classical First Order Logic
- A semantics of evidence for classical arithmetic
- GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION
- Logic for Programming, Artificial Intelligence, and Reasoning
- Cut-elimination and redundancy-elimination by resolution
This page was built for publication: Expansion trees with cut
