Expansion trees with cut

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

zbMATH Keywords

cut eliminationproof theoryHerbrand's theoremexpansion trees

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

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