Tautology elimination, cut elimination, and S5

DOI10.12775/LLP.2017.005MaRDI QIDQ4565826zbMATH OpenOpenAlexFDO

Authors Andrzej Indrzejczak

Publication date 13 June 2018

Published in Logic and Logical Philosophy (Search for Journal in Brave)

Full work available at URL https://doi.org/10.12775/llp.2017.005

zbMATH Keywords

cut eliminationsequent calculusmodal logic S5tautology elimination

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Cut-free double sequent calculus for S5
• Cut Elimination in the Presence of Axioms
• A cut-free simple sequent calculus for modal logic S5
• scientific article; zbMATH DE number 975278
• Cut free sequent calculus for logic S5\(_n\)(ED)

Cites work

• scientific article; zbMATH DE number 3131074 (Why is no real title available?)
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A short and readable proof of cut elimination for two first-order modal logics
• A simple propositional \(\text{S}5\) tableau system
• Cut elimination for GLS using the terminability of its regress process
• Hypersequent calculi for S5: the methods of cut elimination
• Proof methods for modal and intuitionistic logics
• Simple decision procedure for \(\mathbf {S5}\) in standard cut-free sequent calculus
• Structural proof theory. With an appendix by Aarne Ranta

Cited in

(3)

• Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq
• The logicality of equality
• A simple irredundance test for tautological sequents

Describes a project that uses

Uses Software

• Pesca

This page was built for publication: Tautology elimination, cut elimination, and S5

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