On the non-confluence of cut-elimination

DOI10.2178/JSL/1294171002MaRDI QIDQ3083141zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

confluencecut-eliminationfirst-order arithmeticwitness extraction

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(10)

• Herbrand's theorem as higher order recursion
• scientific article; zbMATH DE number 1471986 (Why is no real title available?)
• scientific article; zbMATH DE number 1722658 (Why is no real title available?)
• 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)