# Simplified Integrity Checking for an Expressive Class of Denial Constraints
## 5 Denials with Negated Existential Quantifiers
_transform the resulting formula into a set of extended denials according to the following patterns;_ \(\Phi(Arg)\) _is an expression indicating the body of an NEE in which_ \(Arg\) _occurs;_ \(\overrightarrow{X}\) _and_ \(\overrightarrow{Y}\) _are disjoint sequences of variables:_  
* \(\leftarrow\)__\(A\wedge(B\lor C)\) _is replaced by_ \(\leftarrow\)__\(A\wedge B\) _and_ \(\leftarrow\)__\(A\wedge C\)_;_
* \(\leftarrow\)__\(A\wedge\
eg(B\lor C)\) _is replaced by_ \(\leftarrow\)__\(A\wedge\
eg B\wedge\
eg C\)_;_
* \(\leftarrow\)__\(A\wedge\
eg(B\wedge C)\) _is replaced by_ \(\leftarrow\)__\(A\wedge\
eg B\) _and_ \(\leftarrow\)__\(A\wedge\
eg C\)_;_
* \(\leftarrow\)__\(A\wedge\
eg\exists\overrightarrow{X}\Phi(\
eg\exists\overrightarrow{Y} \left[B\wedge(C\lor D)\right])\) _is replaced by_ \(\leftarrow\)__\(A\wedge\
eg\exists\overrightarrow{X}\Phi(\
eg\exists\overrightarrow{Y} \left[B\wedge C\right])\)_._  
Without loss of generality, we can assume that, for any NEE \(N=\
eg\exists\overrightarrow{X}B\) occurring in an extended denial \(\phi\), the variables \(\overrightarrow{X}\) do not occur outside \(N\) in \(\phi\). This can simply be obtained by renaming the variables appropriately and we refer to such an extended denial as _standardized_. The _level_ of an NEE in an extended denial is the number of NEEs that contain it plus \(1\). The level of a variable \(X\) in a standardized extended denial is the level of the NEE starting with \(\
eg\exists\overrightarrow{X}\), where \(X\) is one of the variables in \(\overrightarrow{X}\), or \(0\) if there is no such NEE. The level of an extended denial is the maximum level of its NEEs, or \(0\) if there is no NEE. In Example 11, the extended denial has level \(1\), \(X\) has level \(0\), and \(Y\) has level \(1\). With a slight abuse of notation, we write in the following \(S\equiv\Psi\) (or \(\Psi\equiv S\)), where \(S=\langle\mathit{IDB},\mathit{IC}\rangle\) is a schema and \(\Psi\) is a set of extended denials, to indicate that, for every database \(D\) based on \(\mathit{IDB}\), \(D\models\mathit{IC}\) if \(D\models\Psi\). We can now claim the correctness of \(\mathsf{Unfold}_{\mathcal{L}_{u}}\). We state the following proposition without a proof, since all steps in Definition 16 are trivially equivalence-preserving. **Proposition 1**. : _Let \(S\in\mathcal{L}_{u}\). Then \(\mathsf{Unfold}_{\mathcal{L}_{u}}(S)\equiv S\)._  
Since the variables under a negated existential quantifier conform with the intuition behind safeness, the unfolding of a schema in which all the clauses are range-restricted yields a set of extended denials that still are safe in this sense. We also note that the language of extended denials is very expressive. In [92], it was shown that _any_ closed formula of the form \(\forall\overrightarrow{X}(\leftarrow\mathit{B})\), where \(B\) is a first-order formula and \(\overrightarrow{X}\) are its open variables, can be equivalently expressed by a set of Prolog rules plus the denial \(\leftarrow\)\(q(\overrightarrow{X})\), where \(q\) is a fresh predicate symbol. The construction is such that, if \(B\) is function-free, then the resulting rule set is also function-free (no skolemization is needed), i.e., it is that of a schema in \(\mathcal{L}_{u}\). The unfolding of the obtained schema is therefore an equivalent set of extended denials. A simplification procedure can now be constructed for extended denials in a way similar to what was achieved in \(\mathcal{L}_{\mathfrak{s}}\). Definition 17: Let \(S\) be a schema in \(\mathcal{L}_{n}\) and \(U\) an update. We define  
\[\mathsf{After}^{U}_{\mathcal{L}_{n}}(S)=\mathsf{Unfold}_{\mathcal{L}_{n}}( \mathsf{After}^{U}(S)).\]  
The optimization step needs to take into account the nesting of NEEs in extended denials. Besides the elimination of disjunctions within NEEs, which is performed by \(\mathsf{Unfold}_{\mathcal{L}_{n}}\), we can also eliminate, from an NEE, equalities and non-equalities referring to variables of lower level with respect to the NEE.