A simple propositional \(\text{S}5\) tableau system
type: Item
instance of: scholarly article
title: A simple propositional \(\text{S}5\) tableau system
zbMATH Open document ID: 0972.03017
DOI: 10.1016/S0168-0072(98)00034-7
author: Melvin Fitting
published in: Annals of Pure and Applied Logic
publication date: 2001-11-09T00:00:00Z
review text: The paper presents a `remarkably simple' tableau system for the modal logic S5 and proves it soundness and weak completeness. The latter means that it captures S5-validity but not logical consequence. Using this tableau system, it is easy to understand why satisfiability in S5 is NP-complete. Also the author hopes that a similar system for first-order S5 could be constructed.
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 1308110
zbMATH Keywords: modal logic
zbMATH Keywords: tableau system
zbMATH Keywords: S5
reviewed by: Valentin Shehtman
MaRDI profile type: Publication
cites work: Failures of the interpolation lemma in quantified modal logic
cites work: Proof methods for modal and intuitionistic logics
cites work: Q4285787
cites work: The Computational Complexity of Provability in Systems of Modal Propositional Logic
full work available at URL: s0168-0072(98)00034-7
OpenAlex ID: W1984799723
description: scientific article; zbMATH DE number 1308110