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