| Abstract: | We study a general framework for query rewriting in the presence of a domain independent first-order logic theory (a knowledge base) over a signature including database and non-database predicates, based on Craig's interpolant and Beth's definability theorem. In our framework queries are (possibly open) domain independent first-order formulas over the extended signature. The database predicates are meant to be closed, i.e., their extensions are the same in every model since they represent a classical finite relational database, whereas the non-database predicates in the ontology are interpreted classically, i.e., their extensions may vary across different models. It is important to notice that all the conceptual modelling languages devised for the designing of information and database systems (such as Entity-Relationship schemas, UML Class diagrams, Object-Role Modelling ORM diagrams, etc) are domain independent: they can be formalised as domain independent first order theories. Given a domain independent knowledge base and a query implicitly definable from the database signature, the framework provides precise semantic conditions to decide the existence of a domain independent first-order logically equivalent reformulation of the query (called exact rewriting) in terms of the database signature, and if so, it provides an effective approach to construct the reformulation based on interpolation using standard theorem proving techniques (e.g., tableau). We are interested in domain independent reformulations of queries because their range-restricted syntax is needed to reduce the original query answering problem to a relational algebra evaluation over the original database, that is, it is effectively executable as an SQL query directly over the database.
Due to the results on the applicability of Beth's theorem and Craig's interpolant, we prove the completeness of our framework in the case of domain independent ontologies and queries expressed in any fragment of first-order logic enjoying finitely controllable determinacy, a stronger property than the finite model property of the logic. If the employed logic does not enjoy finitely controllable determinacy our approach would become sound but incomplete, but still effectively implementable using standard theorem proving techniques. In order to constructively compute the exact domain independent query reformulation we use the tableau based method to find the Craig’s interpolant to compute the from a validity proof of the implication (KB $\land$ Q) $\rightarrow$ (KB $\rightarrow$ Q).
Since description logics knowledge bases are not necessarily domain independent, we have syntactically characterised the domain independent fragment of several very expressive fragments of description logics by enforcing a sort of guarded negation, a very reasonable restriction from the point of view of conceptual modelling. These fragments do also enjoy finitely controllable determinacy.
We have applied this framework not only to query answering under constraints, but also to data exchange and to view update. |
