On finding query rewritings under expressive constraints

We study a general framework for query rewriting in the presence of general FOL constraints, where standard theorem proving techniques (e.g., tableau or resolution) can be used. The framework supports deciding the existence of an equivalent reformulation of a query in terms of a selected set of database predicates, and if so, it provides an effective approach to constructing such a reformulation based on interpolation. It is particularly concerned with applying this framework to finding effectively executable first-order reformulations (i.e., range-restricted reformulations) a la SQL.