A loop-free decision procedure for modal propositional logics K4, S4 and S5 (Q2271187)

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.