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.