The talk will discuss di erent decision procedures for modal logic with nominals and eventualities. This logic has an ExpTime-complete decision problem and is not compact. There is a simple and worst-case optimal decision procedure, which is not practical since it is not incremental. I will discuss two incremental procedures, one worst-case optimal procedure for the fragment without nominals, and one not worst-case optimal procedure for the full logic. A main concern will be the correctness arguments for the procedures. The talk is based on joint work with Mark Kaminski.