Proof Search Tree and Cut Elimination

DOI10.1007/978-3-540-78127-1_28MaRDI QIDQ5452195zbMATH OpenOpenAlexFDO

Authors G. E. Mints

Publication date 25 March 2008

Published in Pillars of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78127-1_28

Mathematics Subject Classification ID

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

Recommendations

• Unwinding a Non-effective Cut Elimination Proof
• Cut Elimination In Situ
• scientific article; zbMATH DE number 7178366
• Analytic cut trees
• Herbrand disjunctions, cut elimination and context-free tree grammars

Cites work

• E theorems
• scientific article; zbMATH DE number 3497842 (Why is no real title available?)
• scientific article; zbMATH DE number 3606451 (Why is no real title available?)
• Unwinding a Non-effective Cut Elimination Proof

Cited in

(5)

• Trees and diagrams of decomposition
• On the non-confluence of cut-elimination
• Functorial bounds for cut elimination inL βω . I
• Tree grammars for the elimination of non-prenex cuts
• On the form of witness terms

This page was built for publication: Proof Search Tree and Cut Elimination

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