A loop-free decision procedure for modal propositional logics K4, S4 and S5 (Q2271187)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A loop-free decision procedure for modal propositional logics K4, S4 and S5 |
scientific article |
Statements
A loop-free decision procedure for modal propositional logics K4, S4 and S5 (English)
0 references
6 August 2009
0 references
Socratic proofs are constructed in guidance of the rules of the calculus of questions [see \textit{A. Wiśniewski}, J. Philos. Log. 33, No. 3, 299--326 (2004; Zbl 1048.03009)]. The author presents a loop-free decision procedure for the modal propositional logics \(\mathbf{K4}\), \(\mathbf{S4}\) and \(\mathbf{S5}\) based on the method of specific Socratic proofs for modal logic. It is shown that the procedure terminates and that it is sound and complete.
0 references
decision procedure
0 references
logic of questions
0 references
method of Socratic proofs
0 references
transitive modal logics
0 references
loop-free procedures
0 references
0 references
