Speaker: Jens Happe

Time: Thursday, Dec 11, 1:30 pm

Place: ASB 9507

Title: Labelled Representations of Modal Formulas

Abstract: Perhaps the most inherent weakness of Automated Reasoning with Tableaux
is their tendency for "thrashing", i.e. repeated reasoning over the
same formulas. We take a look at the modal logic K which offers sufficiently
complex model structures to study thrashing phenomena and their sources.

First, we outline some existing improvements and their shortcomings. We will
then present a new representation formalism for formulas which uses labels instead
of modal operators. Step by step, we will develop a suitable characterization
of models for labelled formulas, and explain why this characterization is suitable
formodal logic K. We compare their respective representation complexity and
give a surprising complexity result for model checking.

This talk will largely follow the informal style of the CL seminars;the results will be presented in an accessible way, with no more formal notation and bothersome details than absolutely necessary; a background in modal logic and/or tableaux reasoning is desirable but not essential.