Tautology elimination, cut elimination, and S5

DOI10.12775/LLP.2017.005zbMATH Open1417.03284OpenAlexW2606283603MaRDI QIDQ4565826FDOQ4565826

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

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)

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)

Cites Work

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

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

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)