Expansion trees with cut
From MaRDI portal
Abstract: Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher-order logic by recording the information of which instances have been chosen for which quantifiers. This compact representation is known in the literature as Miller's expansion tree proof. It is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cuts have been proposed. These extensions are based on graphical formalisms similar to proof nets and are limited to prenex formulas. In this paper we present a new syntactic approach that directly extends Miller's expansion trees by cuts and covers also non-prenex formulas. We describe a cut-elimination procedure for our expansion trees with cut that is based on the natural reduction steps and show that it is weakly normalizing.
Recommendations
Cites work
- A compact representation of proofs
- A new deconstructive logic: linear logic
- A semantics of evidence for classical arithmetic
- Classical proof forestry
- Cut normal forms and proof complexity
- Cut-elimination and redundancy-elimination by resolution
- Exploring the computational content of the infinite pigeonhole principle
- Game semantics and the geometry of backtracking: a new complexity analysis of interaction
- Herbrand-confluence for cut elimination in classical first order logic
- scientific article; zbMATH DE number 1324438 (Why is no real title available?)
- Linear logic
- Logic for Programming, Artificial Intelligence, and Reasoning
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
- On the non-confluence of cut-elimination
- Proof nets for Herbrand's theorem
- Strong normalisation of cut-elimination in classical logic
- System description: GAPT 2.0
- The computational content of arithmetical proofs
- The duality of computation
- The epsilon calculus and Herbrand complexity
Cited in
(16)- A compact representation of proofs
- A natural proof system for Herbrand's theorem
- TBA and tree expansion
- Herbrand's theorem as higher order recursion
- Proof nets for Herbrand's theorem
- scientific article; zbMATH DE number 3871341 (Why is no real title available?)
- scientific article; zbMATH DE number 7447752 (Why is no real title available?)
- Analytic cut trees
- On the Herbrand content of LK
- The true concurrency of Herbrand's theorem
- Herbrand Proofs and Expansion Proofs as Decomposed Proofs
- Deep inference and expansion trees for second-order multiplicative linear logic
- Classical proof forestry
- Extraction of expansion trees
- Herbrand schemes for first-order logic
- A simplified proof of the epsilon theorems
This page was built for publication: Expansion trees with cut
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5236547)
