Tautology Elimination, Cut Elimination, and S5

DOI10.12775/LLP.2017.005zbMath1417.03284OpenAlexW2606283603MaRDI QIDQ4565826

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)

Related Items (1)

Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq

Uses Software

• Pesca

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Cut elimination for GLS using the terminability of its regress process
• Proof methods for modal and intuitionistic logics
• A simple propositional \(\text{S}5\) tableau system
• A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics
• Hypersequent Calculi for S5: The Methods of Cut Elimination
• Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus
• A Computing Procedure for Quantification Theory

This page was built for publication: Tautology Elimination, Cut Elimination, and S5