There are two main methods of completeness proof in modal logic. One may use maximally consistent theories or their algebraic counterparts, on the one hand, or semantic tableaux and their variants, on the other hand. The former method is elegant but not constructive, the latter method is constructive but not elegant.
No takes yet. Share an insight, caveat, or question.
Kit Fine (1975) studied this question.