Non-elementary compression of first-order proofs in deep inference using epsilon-terms
From MaRDI portal
Cites work
- A compact representation of proofs
- A first order system with finite choice of premises
- A proof calculus which reduces syntactic bureaucracy
- A semantics of evidence for classical arithmetic
- A sequent-calculus based formulation of the extended first epsilon theorem
- A system of interaction and structure
- Classical proof forestry
- Combinatorial proofs and decomposition theorems for first-order logic
- Cut elimination inside a deep inference system for classical predicate logic
- Deep inference and symmetry in classical proofs
- Epsilon substitution for first- and second-order predicate logic
- Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)
- Extracting Herbrand disjunctions by functional interpretation
- Herbrand complexity and the epsilon calculus with equality
- Herbrand Proofs and Expansion Proofs as Decomposed Proofs
- Herbrand's theorem as higher order recursion
- scientific article; zbMATH DE number 627412 (Why is no real title available?)
- scientific article; zbMATH DE number 1748963 (Why is no real title available?)
- scientific article; zbMATH DE number 3248792 (Why is no real title available?)
- Lower Bounds on Herbrand's Theorem
- On the Interpretation of Non-Finitist Proofs--Part I
- On the No-Counterexample Interpretation
- Proof nets for Herbrand's theorem
- Recherches sur la théorie de la démonstration.
- Semantics and proof theory of the epsilon calculus
- The epsilon calculus and Herbrand complexity
- The true concurrency of Herbrand's theorem
- Unsound inferences make proofs shorter
This page was built for publication: Non-elementary compression of first-order proofs in deep inference using epsilon-terms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6970282)
