Speaker: Jens Happe

Date: Wednesday, April 30th @ 3:00pm, ASB 9705

A compact formalism for modal logics

Propositional modal logics have established themselves in Automated Reasoning as a family of logics which are more expressive than plain propositional logic, while still decidable (unlike full first-order logic). They allow reasoning on states of affairs in different but related worlds. This makes them suitable formalisms for efficient but complete reasoners on expressive knowledge bases, which indeed have emerged over the last 5-10 years. However, there is still much to be gained in terms of efficiency, as one wants to proceed from knowledge bases with ~10000 facts to knowledge bases with millions of facts.

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.