SCAN is complete for all Sahlqvist formulae

Vendredi 20 septembre 2002 à 10 heures

Salle du conseil de l' Irit

Résumé : SCAN is an algorithm for reducing monadic existential second-order formulae to equivalent simpler (usually first-order) formulae, by elimination of the existentially quantified predicate variables from formulae. The problem whether such equivalent exists for an arbitrarily given monadic existential second-order formulae is undecidqble; so SCAN cannot be always successful. Nevertheless, SCAN is sound, i.e. whenever the algorithm terminates successfully, the resulting formula is equivalent to the original formula. In this work we prove that SCAN works successfully not only for all modal formulae of the  classical Sahlqvist class, but also for all polyadic modal formulas from the generalized Sahlqvist class recently introduced by Vakarelov and myself. At the end of the talk I will discuss some related open questions and directions for further research on the topic.

Retour à la page des séminaires