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.