# Simplified Integrity Checking for an Expressive Class of Denial Constraints
## 5 Denials with Negated Existential Quantifiers
\[\leftarrow p(X)\land\
eg\exists Y\{q(X,Y)\land\
eg\exists Z[r(X,Y,Z) \wedge X=a]\}\] \[\equiv \leftarrow p(X)\land\
eg\exists Y\{q(X,Y)\wedge X=a\land\
eg\exists Z[r(X,Y,Z)]\}\] \[\land\
eg\exists Y[q(X,Y)\wedge X\
eq a]\] \[\equiv \{ \leftarrow p(a)\land\
eg\exists Y[q(a,Y)\land\
eg\exists Zr(a,Y,Z)]\land \
eg\exists Y[q(a,Y)\wedge a\
eq a],\] \[\leftarrow p(X)\wedge X\
eq a\land\
eg\exists Y[X\
eq a\wedge q(X,Y)]\] \[\equiv \{ \leftarrow p(a)\land\
eg\exists Y[q(a,Y)\land\
eg\exists Zr(a,Y,Z)]\land \
eg\exists Y[q(a,Y)\wedge a\
eq a],\] \[\leftarrow p(X)\land X\
eq a\land\
eg\exists Yq(X,Y),\] \[\leftarrow p(a)\land X\
eq a\land X=a\] \[\equiv \{ \leftarrow p(a)\land\
eg\exists Y[q(a,Y)\land\
eg\exists Zr(a,Y,Z)],\] \[\leftarrow p(X)\wedge X\
eq a\land\
eg\exists Yq(X,Y)\]  
In the first step, we applied equality elimination to \(X=a\) at level \(2\). In the second step, we applied the rewrite rule (2) for equality elimination to \(X=a\) at level \(1\). Then, we applied non-equality elimination to \(X\
eq a\) at level \(1\) in the second denial. In the last step, we removed, by standard application of reduction, the last extended denial and the last NEE in the first extended denial, which are clearly tautological. We observe that the body of an NEE is structurally similar to the body of an extended denial. The only difference is that, in the former, there are variables that are quantified at a lower level. According to this observation, such (free) variables in the body of an NEE are to be treated as parameters during the different optimization steps, since, as was indicated on page 2, parameters are free variables. Reduction (Definition 10) can then take place in NEE bodies exactly as in ordinary denials, with the proviso above of treating free variables as parameters. The definition of resolution (Definition 11) can be adapted for extended denials by applying it to general literals instead of literals. Subsumption (Definition 9) can also be applied to extended denials without changing the definition. However, we can slightly modify the notion of subsumption to explore the different levels of NEEs in an extended denial. This is captured by the following definition. Let \(\phi=\leftarrow A\wedge B\) and \(\psi=\leftarrow C\wedge D\) be two extended denials, where \(A\) and \(C\) are (possibly empty) conjunctions of literals and \(B\) and \(D\) are (possibly empty) conjunctions of NEEs. Then \(\phi\) extended-subsums \(\psi\), written \(\phi\overset{\leftarrow}{\leftarrow}\psi\), if both conditions (1) and (2) below hold. (1) \(\leftarrow A\) subsums \(\leftarrow C\) with substitution \(\sigma\). _For every NEE \(\
eg\exists\overrightarrow{X}_{N}\) in \(B\), there is an NEE \(\
eg\exists\overrightarrow{X}_{M}M\) in \(D\) such that \(\gets N\sigma\) is extended-subsumed by \(\gets M\)._  
**Example 13**. : _The extended denial \(\gets p(X)\wedge\
eg\exists Y,Z[q(X,Y)\wedge r(Y,Z)]\) extended-subsumes the extended denial \(\gets p(a)\wedge\
eg\exists T[q(a,T)]\wedge\
eg\exists W[s(T)]\), since \(\gets p(X)\) subsumes \(\leftarrow p(a)\) with substitution \(\{X/a\}\) and, in turn, \(\leftarrow q(a,T)\) subsumes \(\leftarrow q(a,Y)\wedge r(Y,Z)\)._  
This definition encompasses ordinary subsumption, in that it coincides with it if \(B\) and \(D\) are empty. Furthermore, it captures the desired property that if \(\phi\) extended-subsumes \(\psi\), then \(\phi\models\psi\); the reverse, as in subsumption, does not necessarily hold. **Proposition 3**. : _Let \(\phi\) and \(\psi\) be extended denials. If \(\phi\mathrel{\mathop{\kern 0.0 pt\hbox to 0.0 pt{\vbox{\hbox{\scriptsize. }\hbox{ \scriptsize. }}}\kern-1.29 pt\hbox{\scriptsize. }}}\psi\), then \(\phi\models\psi\)._  
Proof. : Let \(\phi,\psi,A,B,C,D\) be as in Definition 19. If \(B\) and \(D\) are empty, the claim holds, since \(\phi\) and \(\psi\) are ordinary denials. The claim also holds if \(D\) is not empty, since \(\leftarrow\ C\) entails \(\gets C\wedge D\). We now show the general claim with an inductive proof on the level of extended denials.