Cut elimination by unthreading

DOI10.1007/S00153-023-00892-4MaRDI QIDQ6139240zbMATH OpenOpenAlexFDO

Authors Gabriele Pulcini

Publication date 18 January 2024

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

classical propositional logiccut eliminationsequent calculus

Mathematics Subject Classification ID

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

Cites work

• A minimal classical sequent calculus free of structural rules
• A note on cut-elimination for classical propositional logic
• Cut elimination for GLS using the terminability of its regress process
• Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq
• Efficient loop-check for backward proof search in some non-classical propositional logics
• Fractional semantics for classical logic
• Gentzen-type systems, resolution and tableaux
• scientific article; zbMATH DE number 4210100 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 3241254 (Why is no real title available?)
• scientific article; zbMATH DE number 3327279 (Why is no real title available?)
• scientific article; zbMATH DE number 7669420 (Why is no real title available?)

This page was built for publication: Cut elimination by unthreading

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