Correcting the tableau procedure for S4

DOI10.1305/NDJFL/1093870631MaRDI QIDQ761443zbMATH OpenOpenAlexFDO

Authors Bangs L. Tapscott

Publication date 1984

Published in Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1305/ndjfl/1093870631

zbMATH Keywords

accessibilityblocked treenormal modal logicpossible worldS4tableau procedure

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Review text

The tableau procedure for normal modal logic is given by Kripke's semantics. S4, which defines the accessibility relation as reflexive and transitive, raises a special problem (infinite tree and then blocked tree). In this paper, the author attempts to correct shortcomings in this procedure. A modified restriction on blockade and equivalence class membership is stated.

Recommendations

• scientific article; zbMATH DE number 3877148
• Corrigendum to: ``A new method to obtain termination in backward proof search for modal logic S4
• A new S4 classical modal logic in natural deduction
• Path calculus in the modal logic S4
• A Polynomial Translation of S4 into T and Contraction-Free Tableaux for S4

Cited in

(3)

• A Polynomial Translation of S4 into T and Contraction-Free Tableaux for S4
• Corrigendum to: ``A new method to obtain termination in backward proof search for modal logic S4
• scientific article; zbMATH DE number 2024627 (Why is no real title available?)

This page was built for publication: Correcting the tableau procedure for S4

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