# Simplified Integrity Checking for an Expressive Class of Denial Constraints
## 4 A Simplification Procedure for Obtaining a Pre-Test
### Simplification in \(\mathcal{L}_{\mathrm{s}}\)
We also refer to the notion of _expansion_[8]: the expansion of a clause consists of replacing every constant or parameter in a database predicate (or variable already appearing elsewhere in database predicates) by a new variable and adding the equality between the new variable and the replaced item. We indicate the expansion of a (set of) denial(s) with a \"+\" superscript. **Example 9**. : _Let \(\phi=\ \leftarrow\ p(X,a,X)\). Then, \(\phi^{+}=\ \leftarrow\ p(X,Y,Z)\wedge Y=a\wedge Z=X\)._  
For a constraint theory \(\Gamma\) in \(\mathcal{L}_{\mathrm{s}}\) and a denial \(\phi\) in \(\mathcal{L}_{\mathrm{s}}\), the notation \(\Gamma\vdash_{R}\phi\) indicates that there is a resolution derivation of a denial \(\phi\) from \(\Gamma^{+}\) and \(\psi^{-}\sqsubseteq\phi\). The \(\vdash_{R}\) procedure is sound; additionally, it is guaranteed to terminate on any input provided that, in each resolution step, the resolvent has at most as many literals as those in the largest denial in \(\Gamma^{+}\) (i.e., by forcing an upper bound on the size of the clauses). We can now provide a possible implementation of an optimization operator that eliminates redundant literals and denials from a given constraint theory \(\Gamma\) assuming that another theory \(\Delta\) holds. Informally, \(\vdash_{R}\), subsumption and reduction are used to approximate entailment. In the following, \(A\sqcup B\) indicates the union of disjoint sets. **Definition 12**. : _Given two constraint theories \(\Delta\) and \(\Gamma\) in \(\mathcal{L}_{\mathrm{s}}\), \(\mathsf{Optimize}^{\Delta}_{\mathcal{L}_{\mathrm{s}}}(\Gamma)\) is the result of applying the following rewrite rules on \(\Gamma\) as long as possible. In the following, \(\phi\), \(\psi\) are denials in \(\mathcal{L}_{\mathrm{s}}\), \(\Gamma^{\prime}\) is a constraint theory in \(\mathcal{L}_{\mathrm{s}}\)._  
\[ \begin{array}{lcl}\{\phi\}\sqcup\Gamma^{\prime}&\Rightarrow&\Gamma^{\prime} \text{ if }\phi^{-}=\text{ true}\\ \{\phi\}\sqcup\Gamma^{\prime}&\Rightarrow&\Gamma^{\prime}\text{ if }(\Gamma^{\prime} \cup\Delta)\vdash_{R}\phi\\ \{\phi\}\sqcup\Gamma^{\prime}&\Rightarrow&\{\phi^{-}\}\sqcup\Gamma^{\prime} \text{ if }\phi\
eq\phi^{-}\
eq\text{ true}\\ \{\phi\}\sqcup\Gamma^{\prime}&\Rightarrow&\{\psi^{-}\}\sqcup\Gamma^{\prime} \text{ if }(\{\phi\}\sqcup\Gamma^{\prime}\cup\Delta)\vdash_{R}\psi\text{ and }\psi^{-}\sqsubset\phi\end{array} \]  
The first two rules attempt the elimination of a whole denial, whereas the last two try to remove literals from a denial. We can now fully define simplification for \(\mathcal{L}_{\mathrm{s}}\):  
**Definition 13**. : _Let \(S=\langle IDB,\Gamma\rangle\in\mathcal{L}_{\mathrm{s}}\) and \(U\) be an update in \(\mathcal{L}_{\mathrm{s}}\) with respect to \(S\). Let \(\mathsf{Unfold}_{\mathcal{L}_{\mathrm{s}}}(S)=\langle\mathcal{O},\Gamma^{ \prime}\rangle\). We define \(\mathsf{Simp}^{U}_{\mathcal{L}_{\mathrm{s}}}(S)=\mathsf{Optimize}^{U}_{ \mathcal{L}_{\mathrm{s}}}(\mathsf{After}^{U}_{\mathcal{L}_{\mathrm{s}}}(S))\)._  
Clearly, \(\mathsf{Simp}^{U}_{\mathcal{L}_{\mathrm{s}}}(S)\) is a CWP of \(S\) with respect to \(U\). **Example 10**. : _Consider again Example 7. The reduction of each denial in \(\mathsf{After}^{U}_{\mathcal{L}_{\mathrm{s}}}(\{\phi\})\) generates the following set._  
\[ \begin{array}{lcl}\{&\leftarrow&b(X,Y)\wedge b(X,Z)\wedge Y\
eq Z,\\ &\leftarrow&b(\mathbf{i},Y)\wedge Y\
eq\mathbf{t},\\ &\leftarrow&b(\mathbf{i},Z)\wedge\mathbf{t}\
eq Z&\}.\end{array} \]  
_Then, the third denial is removed, as it is subsumed by the second one; the first constraint is subsumed by \(\phi\) and, thus, removed, so \(\mathsf{Simp}^{U}_{\mathcal{L}_{\mathrm{s}}}(\{\phi\})=\ \{\gets b(\mathbf{i},Y)\wedge Y\
eq\mathbf{t}\}\). This result indicates that, for the database to be consistent after update \(U\), a book with ISBN \(\mathbf{i}\) must not be already associated with a title \(Y\) different from \(\mathbf{t}\)._