Gao, Feng, and George Tourlakis. 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.