Modal definability of first-order formulas and its application to knowledge bases

The talk is about an application of results from a branch of modal logic known as Modal Definability Theory to the problem of query answering in first-order theories. Modal definability of a first-order formula $q(x)$ means the existence of a modal formula that is valid at a world of a Kripke frame iff $q(x)$ is true at this world. In first-order logic, the following problem makes sense: given a first-order theory $T$ and a formula $q(x)$, called a query to $T$ in this context, find all constants $c$ (called answers to the query) for which $T$ entails $q(c)$. It was recently discovered that the two notions are closely related, and results from modal definability can be used for query answering in first-order theories and, in particular, in knowledge bases. The framework can be generalized also to queries with several free variables. We shall also describe a family of conjunctive queries that can be efficiently answered without rise of complexity (on the contrary, the general query answering problem is exponentially harder). This is a joint work with Stanislav Kikot.