Stanislav Kikot

On modal definability of first-order formulas with many free variables and its application to query answering in expressive description logics

The correspondence between modal axioms and first-order Kripke frame conditions is the heart of modal logic. Developed in 1960s, it is still a common tool for proving the completeness of many modal calculi. A typical modern example of its application is different logics of multi-agent systems for reasoning about agents' knowledge, belief, intensions and cooperative actions.

There are two traditional kinds of such a correspondence, namely, the global correspondence between modal formulas and closed first-order formulas and the local correspondence between modal formulas and first-order formulas with one free variable.

In "Tools and Techniques of Modal Logic" by Marcus Kracht (~1998) the definition of the local correspondence between finite tuples of modal formulas and first-order formulas with several free variables appeared for the first time. There the basic properties of this correspondence were stated and proved, and a special calculus (so called "Calculus of internal descriptions") was devised to infer the instances of such a correspondence. Also this correspondence was used in this book to give a formal proof to the claim, which is now known as "Kracht's theorem."

Until now, this correspondence was used only as a technical tool for proving similar theorems. But recently some query answering algorithms relying on the classical correspondence theory for first-order formulas with one free variable were introduced by E. Zolin.

Obviously this restriction can be overcome by considering a more general kind of modal definability. And here is the starting point of our work. Our aim is to advance in the correspondence theory for first-order formulas with free variables as far as possible, and to apply it to answering the queries with many answer variables.