  A second kind of complication is technical. There is a wide variety in the choices one can make in the semantics for quantified modal logic, and the proof that a system of rules is correct for a given choice can be difficult. The work of Corsi (2002) and Garson (2005) goes some way towards bringing unity to this terrain, and Johannesson (2018) introduces constraints that help reduce the number of options; nevertheless the situation still remains challenging.