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. doi:10.18778/0138-0680.44.3.4.03