Incremental Decision Procedures for Modal
      Logic with Nominals and Eventualities

                                  Gert Smolka

                               Saarland University
                           smolka@ps.uni-saarland.de

    The talk will discuss different decision procedures for modal logic with nom-
inals 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 nomi-
nals, 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.