Dynamic Model checking for Discourse Representation Structures with pluralities
Model checking for First Order Logic is a computationally demand- ing task. Matters become worse in systems that typically yield fairly large and complex formulas, and that also include the representation of pluralities. This is the case of Discourse Representation Theory (Kamp and Reyle 1993), in which representations encode discourse chunks and deal with various plural phenomena. Not surprisingly, there are virtu- ally no model checkers for DRT. This paper proposes a dynamic model checking strategy that reduces the search space and allows to evaluate non-trivial DRT representations in larger models.