A. Indrzejczak, “Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus”, B Sect Log, vol. 45, no. 2, pp. 125–140, Jun. 2016.