# Simplified Integrity Checking for an Expressive Class of Denial Constraints
## 5 Denials with Negated Existential Quantifiers
Definition 18: Let \(A,B,C\) be (possibly empty) conjunctions of general literals, \(\overrightarrow{Y}\), \(\overrightarrow{Z}\) disjoint (sequences of) variables, \(W\) a variable of level lower than the level of \(\overrightarrow{Z}\), and \(\Phi(\mathit{Arg})\) an expression indicating an NEE in which \(\mathit{Arg}\) occurs. The following rewrite rules are, respectively, the equality elimination and non-equality elimination rules. \[ \begin{array}{l}\leftarrow A\wedge\Phi(\
eg\exists\overrightarrow{Y}[B \wedge\
eg\exists\overrightarrow{Z}(C\wedge W=c)])\ \ \Rightarrow\\ \leftarrow A\wedge\Phi(\
eg\exists\overrightarrow{Y}[B\wedge W=c\wedge\
eg \exists\overrightarrow{Z}(C)\wedge\
eg\exists\overrightarrow{Y}[B\wedge W \
eq c])\\ \leftarrow A\wedge\Phi(\
eg\exists\overrightarrow{Y}[B\wedge\
eg\exists \overrightarrow{Z}(C\wedge W\
eq c)])\ \ \Rightarrow\\ \leftarrow A\wedge\Phi(\
eg\exists\overrightarrow{Y}[B\wedge W\
eq c\wedge \
eg\exists\overrightarrow{Z}(C)]\wedge\
eg\exists\overrightarrow{Y}[B \wedge W=c])\end{array} \]  
The above (non-)equality elimination rewrite rules are equivalence-preserving, as stated below. Proposition 2: Let \(\psi\) be an extended denial and \(\psi^{\prime}\) (resp. \(\psi^{\prime\prime}\)) be the extended denial obtained after an application of the equality (resp. non-equality) elimination rule. Then \(\psi\equiv\psi^{\prime}\) and \(\psi\equiv\psi^{\prime\prime}\). Proof: Using the notation of Definition 18, we have the following:  
\[ \begin{array}{l}\
eg\exists\overrightarrow{Y}[B\wedge\
eg\exists \overrightarrow{Z}(C\wedge W=c)]\\ \equiv\ \ \
eg\exists\overrightarrow{Y}[B\wedge(W=c\lor W\
eq c)\wedge\
eg \exists\overrightarrow{Z}(C\wedge W=c)]\\ \equiv\ \ \
eg\exists\overrightarrow{Y}[B\wedge W=c\wedge\
eg\exists \overrightarrow{Z}(C\wedge W=c)]\wedge\\ \equiv\ \ \
eg\exists\overrightarrow{Y}[B\wedge W\
eq c\wedge\
eg\exists \overrightarrow{Z}(C\wedge W=c)]\\ \equiv\ \ \
eg\exists\overrightarrow{Y}[B\wedge W=c\wedge\
eg\exists \overrightarrow{Z}(C)]\wedge\
eg\exists\overrightarrow{Y}[B\wedge W\
eq c] \end{array} \]  
In the first step, we added the tautological conjunct \((W=c\lor W\
eq c)\). In the second step, we used [PERSON]'s laws in order to eliminate the disjunction (as in the definition of \(\mathsf{Unfold}_{\mathcal{L}_{n}}\)). The formula \(W=c\wedge\
eg\exists\overrightarrow{Z}(C\wedge W=c)\) can be rewritten as \(W=c\wedge\
eg(\exists\overrightarrow{Z}C\wedge W=c)\), and then as \(W=c\wedge(\
eg\exists\overrightarrow{Z}(C)\lor W\
eq c)\), which, with a resolution step, results in the first NEE in the last extended denial. Similarly, \(W\
eq c\wedge\
eg\exists\overrightarrow{Z}(C\wedge W=c)\) can be rewritten as \(W\
eq c\wedge(\
eg\exists\overrightarrow{Z}(C)\lor W\
eq c)\), which results (by absorption) in the second NEE in the last extended denial. The proof is similar for non-equality elimination. In cases where only levels \(0\) and \(1\) are involved, the rules look simpler. For example, equality elimination can be conveniently formulated as follows. \[ \begin{array}{l}\leftarrow B\wedge\
eg\exists\overrightarrow{X}[C\wedge W= c]\ \ \ \Rightarrow\ \ \ \ \{\begin{array}{l}\leftarrow B\{W/c\}\wedge\
eg\exists \overrightarrow{X}C\{W/c\}\\ \leftarrow B\wedge W\
eq c\end{array}\}.\end{array}  \tag{2}\]Although (non-)equality elimination does not necessarily shorten the input formula (in fact, it can also lengthen it), it always reduces the number of literals in higher-level NEEs. Therefore, convergence to termination can still be guaranteed if this rewrite rule is applied during optimization. Repeated application of such rules \"pushes\" outwards the involved (non-)equalities until they reach an NEE whose level is the same as the level of the variable in the (non-)equality. Then, in case of an equality, the usual equality elimination step of reduction can be applied. The following rewrites show the propagation of a variable of level 0 (X) from level \(2\) to level \(0\) via two equality eliminations and one non-equality elimination.