=Paper=
{{Paper
|id=None
|storemode=property
|title=Incremental Decision Procedures for Modal Logic with Nominals and Eventualities
|pdfUrl=https://ceur-ws.org/Vol-745/invited_paper_2.pdf
|volume=Vol-745
|dblpUrl=https://dblp.org/rec/conf/dlog/Smolka11
}}
==Incremental Decision Procedures for Modal Logic with Nominals and Eventualities==
<pdf width="1500px">https://ceur-ws.org/Vol-745/invited_paper_2.pdf</pdf>
<pre>
    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.

</pre>