Metalogical formalization of Dynamic Logics
Dynamic logics are popular as target systems for semantics construction. There is quite a ariety of them:
- DRT (Kamp & Reyle) and variants (including sDRT and lamba-DRT)
- DPL (Gronendijk and Stokof) and variants (includeing DMG)
- ... it would be nice if the LATIN logic atlas had some of these logics. The main problem is that we cannot just use the LF metalogical framework directly, but have to extend it with dynammic primitieves. This makes things a lot harder. @dmueller has already worked a bit on this, so he can supervise.