Speaker: Jens Happe
Date: Wednesday, April 30th @ 3:00pm, ASB 9705
A compact formalism for modal logics
One bottleneck is that the conventional definition of models for modal formulas requires that variable assignments must be spelled out explicitly for all possible worlds, of which there may be exponentially many. We present an approach to circumvent this problem. Our models allow us to specify variable assignments over ``subspaces'' of the entire space of worlds, thus producing models of considerably reduced size, but also reducing the amount of repeated reasoning in ``similar'' worlds and thus reducing the time complexity of reasoning as well.
As a drawback, consistency checking becomes more involved, and algorithms to generate models for formulas are also considerably more complicated. In this talk, rather than developing the entire formalism, we will look at the essential ideas and illustrate the model finding algorithm through a typical example. The talk is hands-on, with no knowledge required beyond basic propositional logic.