# Simplified Integrity Checking for an Expressive Class of Denial Constraints
## 4 A Simplification Procedure for Obtaining a Pre-Test
### The Core Language \(\mathcal{L}_{5}\)
This will require the introduction of further operators and procedures, which are sketchily described in Figure 3. In particular, the overall procedure receives a schema \(S\) and an update \(U\) and first transforms the schema in ato new schema \(S^{\prime}\), whose integrity constraints hold in the state before the update if and only if the original constraints in \(S\) hold in the updated state. Then, the intensional database in \(S^{\prime}\) is completely eliminated (through \"unfolding\"), because its definitions are going to be embedded in the integrity constraints themselves, thereby producing a set of integrity constraints \(\Gamma\). Finally, the Optimize operator tries to remove all redundancies from \(\Gamma\) by eliminating literals as well as whole denials as much as possible. This is done by exploiting the consistency assumption, i.e., the fact that the original integrity constraints in \(S\) hold before the update; to do this, Optimize receives as input the integrity constraints in \(S\) after embedding the definitions of its intensional database in the constraints (again, through unfolding), which are represented by the set \(\Delta\) in the sketch. The overall output is the set of integrity constraints \(\Gamma^{*}\) from which the redundancies are removed. Generating Weakest Preconditions in \(\mathcal{L}_{\mathsf{s}}\)  
The following syntactic transformation, After, generates a WP. **Definition 7** (After). : _Let \(S=\langle IDB,\Gamma\rangle\) be a schema and \(U\) an update \(p(\overrightarrow{X})\Leftarrow p^{U}(\overrightarrow{X})\)._  
* _Let us indicate with_ \(\Gamma^{U}\) _a copy of_ \(\Gamma\) _in which any atom_ \(p(\overrightarrow{t})\) _is simultaneously replaced by the expression_ \(p^{U}(\overrightarrow{t})\) _and every intensional predicate_ \(q\) _is simultaneously replaced by a new intensional predicate_ \(q^{U}\) _defined in_ \(\operatorname{IDB}^{U}\) _below._
* _Similarly, let us indicate with_ \(\operatorname{IDB}^{U}\) _a copy of_ \(\operatorname{IDB}\) _in which the same replacements are simultaneously made, and let_ \(\operatorname{IDB}^{*}\) _be the biggest subset of_ \(\operatorname{IDB}\cup\operatorname{IDB}^{U}\) _including only definitions of predicates on which_ \(\Gamma^{U}\) _depends._  
_We define_ \(\operatorname{After}^{U}(S)=\langle\operatorname{IDB}^{*},\Gamma^{U}\rangle\)_._  
**Example 5**. : _Consider the updates and \(\operatorname{IDB}\) definitions of Example 1. Let schema \(S_{1}\) be \(\langle\operatorname{IDB}_{1},\Gamma_{1}\rangle\), where \(\Gamma_{1}=\{\gets p(X)\wedge q(X)\}\) states that \(p\) and \(q\) are mutually exclusive. We have \(\operatorname{After}^{U_{1}}(S_{1})=\langle\operatorname{IDB}_{1},\Gamma_{1}^{ U_{1}}\rangle\), where \(\Gamma_{1}^{U_{1}}=\{\gets p^{\prime}(X)\wedge q(X)\}.\) We replace \(p^{\prime}(X)\) by its defining formula and thus omit the intensional database:_  
\[\operatorname{After}^{U_{1}}(\Gamma_{1})=\Sigma= \{ \leftarrow p(X)\wedge q(X),\] \[\leftarrow X=a\wedge q(X)\quad\}.\]  
Clearly, \(\operatorname{After}^{U}(S)\) is a WP of \(S\) with respect to \(U\), and, trivially, a CWP. For \(\mathcal{L}_{\mathsf{s}}\), we use _unfolding_[85] to replace every intensional predicate by its definition until only extensional predicates appear. To this end, we use the \(\mathsf{Unfold}_{\mathcal{L}_{\mathsf{s}}}\) operator below. Figure 3: Sketch of the main blocks in the simplification procedure \(\mathsf{Simp}_{\mathcal{L}_{\mathsf{s}}}\). **Definition 8** (Unfolding). : _Let \(S=\langle\mathit{IDB},\Gamma\rangle\) be a database schema in \(\mathcal{L}_{\mathsf{s}}\). Then, \(\mathsf{Unfold}_{\mathcal{L}_{\mathsf{s}}}(S)\) is the schema \(\langle\mathcal{O},\Gamma^{\prime}\rangle\), where \(\Gamma^{\prime}\) is the set of denials obtained by iterating the two following steps as long as possible:_  
1. _replace, in_ \(\Gamma\)_, each atom_ \(p(\overrightarrow{t})\) _by_ \(F^{p}\{\overrightarrow{X}/\overrightarrow{t}\}\)_, where_ \(F^{p}\) _is_ \(p\)_'s defining formula and_ \(\overrightarrow{X}\) _its head variables.