# Simplified Integrity Checking for an Expressive Class of Denial Constraints
## 5 Denials with Negated Existential Quantifiers  
In the definition of \(\mathcal{L}_{\mathrm{s}}\), we limited the level of interaction between negation and existential quantification in the constraint theories. We now relax this limitation and extend the syntax of denials so as to allow the presence of negated existential quantifiers. The simplification procedure can be adapted to such cases, provided that its components are adjusted so as to handle conjuncts starting with a negated existential quantifier. In this section, we address the problem of simplification of integrity constraints in _hierarchical_ databases, in which all clauses are range-restricted and the schemata are non-recursive, but there is no other restriction on the occurrence of negation. We refer to the language of such schemata as \(\mathcal{L}_{n}\). Definition 14 (\(\mathcal{L}_{n}\)): Let \(S\) be a schema. \(S\) is in \(\mathcal{L}_{n}\) if its starred dependency graph is acyclic. Similarly to the previous section, we summarize the notation and operators used in this section in tabular form (see Table 2), which add to those summarized in Table 1. A diagram showing the main blocks composing the simplification procedure in \(\mathcal{L}_{n}\) would look exactly like the one shown in Figure 3, after taking care of replacing each occurrence of \(\mathcal{L}_{s}\) with \(\mathcal{L}_{n}\). Unfolding predicates in integrity constraints with respect to their definitions cannot be done in the same way as \(\mathsf{Unfold}_{\mathcal{L}_{S}}\). For this purpose, we extend the syntax of denials so as to allow negated existential quantifiers to occur in literals. Definition 15 (Extended denials): _A negated existential expression or NEE is an expression of the form \(\
eg\exists\overrightarrow{X}B\), where \(B\) is called the body of the NEE, \(\overrightarrow{X}\) are some (possibly all) of the variables occurring in \(B\), and \(B\) has the form \(L_{1}\land\ldots\land L_{n}\), where each \(L_{i}\) is a general literal, i.e., either a literal or an NEE._  
_A formula of the form \(\forall\overrightarrow{X}(\leftarrow B)\), where \(B\) is the body of an NEE and \(\overrightarrow{X}\) are some (possibly all) of the free variables in \(B\), is called an extended denial. When there is no ambiguity on the variables in \(\overrightarrow{X}\), extended denials are simply written \(\leftarrow B\)._  
Example 11: _The formula \(\leftarrow\)parent\((X)\land\
eg\exists Ychild\_of(X,Y)\) is an extended denial. It reads as follows: there is inconsistency if there is a parent \(X\) that does not have a child. Note that this is different from the (non-range-restricted) denial \(\leftarrow\)parent\((X)\land\
eg child\_of(X,Y)\), which states that if \(X\) is a parent then all individuals must be his/her children._  
We observe that variables under a negated existential quantifier conform with the intuition behind safeness, so we could conclude that the first formula in Example 11 is safe, whereas the second one is not. The framework we have defined so far is very expressive, since it captures the most common and useful kinds of dependencies, such as TGDs and EGDs. A TGD is a formula of the form \(\forall\overrightarrow{X}(\phi(\overrightarrow{X})\rightarrow\exists \overrightarrow{Y}\psi(\overrightarrow{X},\overrightarrow{Y}))\), where \(\phi(\overrightarrow{X})\) is a conjunction of atomic formulas, all with variables among the variables in \(\overrightarrow{X}\); every variable in \(\overrightarrow{X}\) appears in \(\phi(\overrightarrow{X})\) (but