Indrzejczak, A. “Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus”. Bulletin of the Section of Logic, vol. 45, no. 2, June 2016, pp. 125–140, doi:10.18778/0138-0680.45.2.05.