Formalization and correctness of the CQC method

Abstract

In this report we formalize a new method that checks Query Containment for queries with negated IDB and EDB predicates as well as equality, inequality and order comparisons. The generality of our approach allows also our method to deal straightforwardly with query containment under constraints. We prove soundness and completeness of success and of failure of our method and we characterize the databases where these properties hold.