On the non-confluence of cut-elimination

DOI10.2178/JSL/1294171002zbMATH Open1220.03048OpenAlexW2152266130MaRDI QIDQ3083141FDOQ3083141

Authors: Matthias Baaz, Stefan Hetzl 

Publication date: 18 March 2011

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2178/jsl/1294171002

Recommendations

• On the form of witness terms
• Proof Search Tree and Cut Elimination
• Herbrand-confluence
• The computational content of arithmetical proofs
• Unwinding a Non-effective Cut Elimination Proof

zbMATH Keywords

confluencecut-eliminationfirst-order arithmeticwitness extraction

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• The consistency of arithmetics
• The number of proof lines and the size of proofs in first order logic
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Title not available (Why is that?)
• Theorem Proving via General Matings
• Extracting Herbrand disjunctions by functional interpretation

Cited In (10)

• Herbrand's theorem as higher order recursion
• Title not available (Why is that?)
• Title not available (Why is that?)
• Unsound inferences make proofs shorter
• On the form of witness terms
• Herbrand-confluence for cut elimination in classical first order logic
• Herbrand-confluence
• The computational content of arithmetical proofs
• Expansion trees with cut
• Unwinding a Non-effective Cut Elimination Proof

This page was built for publication: On the non-confluence of cut-elimination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3083141)