# 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}}\)  
The result returned by After\({}_{\mathcal{L}_{\mathrm{s}}}\) may contain redundant parts (e.g., \(a=a\)) and does not exploit the consistency assumption. For this purpose, we define a transformation Optimize\({}_{\mathcal{L}_{\mathrm{s}}}\) that optimizes a given constraint theory using a set of trusted hypotheses. We describe here an implementation in terms of sound and terminating rewrite rules. Among the tools we use are subsumption, reduction, and resolution. **Definition 9** (Subsumption). : _Given two denials \(\phi_{1}\) and \(\phi_{2}\), \(\phi_{1}\) subsumes \(\phi_{2}\) (via \(\sigma\)), written \(\phi_{1}\sqsubseteq\phi_{2}\), if there is a substitution \(\sigma\) such that each literal in \(\phi_{1}\sigma\) occurs in \(\phi_{2}\). The subsumption is strict, written \(\phi_{1}\sqsubset\phi_{2}\), if \(\phi_{1}\) is not a variant of \(\phi_{2}\)._  
The subsumption algorithm (see, e.g., [86]), besides checking subsumption, also returns the substitution \(\sigma\). As is well known, the subsuming denial implies the subsumed one. **Example 8**. : \(\leftarrow\)__\(p(X,Y)\wedge q(Y)\)__\(\mathit{subsumes}\leftarrow\)__\(p(X,b)\wedge X\
eq a\wedge q(b)\) _via \(\{Y/b\}\)._  
_Reduction_[87] characterizes the elimination of redundancies within a single denial. **Definition 10** (Reduction). : _For a denial \(\phi\), the reduction \(\phi^{-}\) of \(\phi\) is the result of applying the following rules on \(\phi\) as long as possible, where \(L\) is a literal, \(c_{1},c_{2}\) are distinct constants, \(X\) is a bound variable, \(t\) is a term, \(A\) is an atom, \(C\), \(D\) (possibly empty) are conjunctions of literals, and_ vars _indicates the set of bound variables occurring in its argument._  
\[ \begin{array}{rcl}\leftarrow\ L\wedge C&\Rightarrow&\leftarrow\ C\ \ \ \text{if $L$ is of the form $t=t$ or $c_{1}\
eq c_{2}$}\\ \leftarrow\ L\wedge C&\Rightarrow&\mathit{true}\ \ \text{if $L$ is of the form $t\
eq t$ or $c_{1}=c_{2}$}\\ \leftarrow\ X=t\wedge C&\Rightarrow&\leftarrow\text{$C\{X/t\}$}\\ \leftarrow\ A\land\
eg A\wedge C&\Rightarrow&\mathit{true}\\ \leftarrow\ C\wedge D&\Rightarrow&\leftarrow\ D\ \ \ \text{if $(\leftarrow) \sqsubset(\leftarrow\text{$D$})$ with a substitution $\sigma$ s.t.}\\ &&\text{dom}(\sigma)\cap\text{vars}(D)=\emptyset\end{array} \]  
Clearly, \(\phi^{-}\equiv\phi\). The last rewrite rule is called subsumption factoring [88] and includes the elimination of duplicate literals from a denial as a special case. An additional rule for handling parameters may be considered in the reduction process:  
\[\leftarrow\mathbf{a}=c_{1}\wedge C\ \ \ \Rightarrow\ \ \leftarrow\mathbf{a}=c_{1}\wedge C\{ \mathbf{a}/c_{1}\} \tag{1}\]  
This may replace parameters with constants and possibly allow further reduction. For example, the denial \(\leftarrow\mathbf{a}=c\wedge b=\mathbf{a}\) would be transformed into \(\leftarrow\mathbf{a}=c\wedge b=c\), and, thus, into \(\mathit{true}\), since \(b\) and \(c\) are different constants. We now briefly recall the definition of resolvent and derivation for the well-known principle of _resolution_[89; 90] and cast it to the context of deductive databases. **Definition 11**. : _Let \(\phi^{\prime}_{1}=\leftarrow\)__\(L_{1}\wedge\ldots\wedge L_{m}\), \(\phi^{\prime}_{2}=\leftarrow\)__\(M_{1}\wedge\ldots\wedge M_{n}\) be two standardized apart variants of denials \(\phi_{1},\phi_{2}\). If \(\theta\) is a mgu of \(\{L_{i},\
eg M_{j}\}\), then the clause_  
\[\leftarrow(L_{1}\wedge\ldots\wedge L_{i-1}\wedge L_{i+1}\wedge\ldots L_{m} \wedge M_{1}\wedge\ldots\wedge M_{j-1}\wedge M_{j+1}\wedge\ldots\wedge M_{n})\theta\]  
_is a binary resolvent of \(\phi_{1}\) and \(\phi_{2}\) and \(L_{i}\), \(M_{j}\) are said to be the literals resolved upon._  
The resolution principle is a sound inference rule, in that a resolvent is a logical consequence of its parent clauses, and preserves range restriction [91].