Cut elimination by unthreading

DOI10.1007/s00153-023-00892-4OpenAlexW4386966222MaRDI QIDQ6139240

Gabriele Pulcini

Publication date: 18 January 2024

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-023-00892-4

zbMATH Keywords

cut eliminationsequent calculusclassical propositional logic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Cut elimination for GLS using the terminability of its regress process
• A minimal classical sequent calculus free of structural rules
• Gentzen-type systems, resolution and tableaux
• Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq
• A note on cut-elimination for classical propositional logic
• FRACTIONAL SEMANTICS FOR CLASSICAL LOGIC
• Efficient loop-check for backward proof search in some non-classical propositional logics

This page was built for publication: Cut elimination by unthreading