On the non-confluence of cut-elimination
From MaRDI portal
Publication:3083141
DOI10.2178/jsl/1294171002zbMath1220.03048OpenAlexW2152266130MaRDI QIDQ3083141
Publication date: 18 March 2011
Published in: The Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2178/jsl/1294171002
Related Items
UNSOUND INFERENCES MAKE PROOFS SHORTER, Herbrand's theorem as higher order recursion, The computational content of arithmetical proofs, On the form of witness terms, Expansion trees with cut
Cites Work
- Unnamed Item
- Unnamed Item
- The number of proof lines and the size of proofs in first order logic
- Extracting Herbrand disjunctions by functional interpretation
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Theorem Proving via General Matings
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- The consistency of arithmetics