Gao, F.; Tourlakis, G. A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics. B Sect Log 2015, 44 (3/4), 131–147. https://doi.org/10.18778/0138-0680.44.3.4.03.