Indrzejczak A. Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus. B Sect Log. 2016;45(2):125–140. doi:10.18778/0138-0680.45.2.05