Interpolation and Query Rewriting

We overview applications of Craig interpolation and Beth definability to simplifying logical expressions or database queries. From the perspective of the theory of interpolation and definability the results give a number of new angles. First, they give a different take on what it means to make definability or interpolation results effective, looking at algorithms that take a proof as input and return an interpolant or explicit definition as output. Secondly, they relate interpolation and definability to preservation theorems in model theory: interpolation and definability theorems are the basis for many “semantics-to-syntax” results, relating a semantic property of a formula to its equivalence with a certain syntactic form. Thirdly, they motivate new forms of interpolation and definability, focusing on syntactic forms that are of interest in databases.