A simple propositional S5 tableau system

DOI10.1016/S0168-0072(98)00034-7MaRDI QIDQ1295438zbMATH OpenOpenAlexFDO

Authors Melvin Fitting

Publication date 9 November 2001

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0168-0072(98)00034-7

zbMATH Keywords

modal logicS5tableau system

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45)

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.

Recommendations

• A simple tableau system for the logic of elsewhere
• scientific article; zbMATH DE number 2209446
• Publication:4731168
• scientific article; zbMATH DE number 5263148
• A cut-free simple sequent calculus for modal logic S5

Cites work

• Failures of the interpolation lemma in quantified modal logic
• scientific article; zbMATH DE number 534879 (Why is no real title available?)
• Proof methods for modal and intuitionistic logics
• The Computational Complexity of Provability in Systems of Modal Propositional Logic

Cited in

(11)

• Efficient SAT-based minimal model generation methods for modal logic S5
• Dugundji's theorem revisited
• A deep inference system for the modal logic S5
• Modal logic S5 in answer set programming with lazy creation of worlds
• scientific article; zbMATH DE number 94918 (Why is no real title available?)
• Tautology elimination, cut elimination, and S5
• A simple tableau system for the logic of elsewhere
• scientific article; zbMATH DE number 4116497 (Why is no real title available?)
• Modal logic S5 satisfiability in answer set programming
• A simple embedding of T into double S5
• Realizations and LP

This page was built for publication: A simple propositional \(\text{S}5\) tableau system

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