SQEMA: a SQEMA: a new algorithm for computing correspondences of modal formula

Prof. Valentin Goranko (Rand Afrikaans University)

CSL SEMINAR SERIES

DATE: 2004-12-02
TIME: 16:00:00 - 17:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.

ABSTRACT:
Propositional modal formulae define on Kripke frames universal monadic second-order properties. Some of them, however, are first-order definable. Such are, for instance, all Sahlqvist formulae, recently extended by us to so called inductive and complex formulae.

In terms of frame validity, modal formulae express universal monadic second-order properties, but in many important cases, these have first-order equivalents. This is important for both logical and computational reasons, because first-order logic is much better studied, and there are more computational tools developed for it, than monadic second-order logic.

Furthermore, often first-order definability goes together with canonicity, which in turn implies completeness of logics axiomatized with such formulae. A general result on both first-order definability and canonicity of a large syntactic class of modal formulae is the celebrated Sahlqvist theorem.

Proving first-order definability of modal formulae amounts to elimination of second-order quantifiers. Two algorithms have been developed and implemented for elimination of predicate quantifiers in second-order logic: SCAN, based on a constraint resolution procedure, and DLS, based on a logical equivalence established by Ackermann.

We have recently introduced a new algorithm, SQEMA, for computing first-order equivalents, and at the same time proving canonicity, of modal formulae. Like DLS, it uses (a modal version of) Ackermann's lemma, but unlike both SCAN and DLS it works directly on modal formulae and thus avoids introduction of Skolem functions and the subsequent problem of unskolemization. In return of being so specialized, it is more transparent and flexible, easier to use and extend, less dependent on the syntactic shape of the formulae, and has greater scope of applicability on modal formulae than either of the others.

Moreover, we have proved that all modal formulae on which SQEMA succeeds are canonical, thus not only advancing the tools for automatic translation, but also introducing a new, purely algorithmic approach to proving completeness via canonicity in modal logic and thus, in particular, establishing the most general completeness result in modal logic so far.

In this talk I will present the core algorithm and illustrate it with some examples. Time permitting, I will also discuss issues such as correctness, completeness for important classes of formulae, and canonicity of the successfully computed formulae.