# Simplified Integrity Checking for an Expressive Class of Denial Constraints
## 3 Relational and Deductive Databases
In the context of deductive databases, however, it is customary to express integrity constraints in some canonical form; we adopt here the denial form, which gives a clear indication of what must not occur in the database. **Definition 1** (Schema, database). : _A database schema\(S\) is a pair \(\langle IDB,IC\rangle\), where IDB (the intensional database) is a finite set of range-restricted rules, and IC (the constraint theory) is a finite set of denials. A database\(D\) on \(S\) is a pair \(\langle IDB,EDB\rangle\), where EDB (the extensional database) is a finite set of facts; \(D\) is said to be based on IDB._  
If the \(IDB\) is understood, the database is identified with \(EDB\) and the schema with IC. For the semantics of a deductive database, we refer to standard texts, such as [77]. There are database classes for which the existence of a unique _intended_ minimal model is guaranteed. One such class is that of _stratified databases_, i.e., those in which no predicatedepends negatively on itself. This can be checked syntactically by building a graph with a node for each predicate and an arc between \(p\) and \(q\) each time \(p\) is in the body and \(q\) in the head of the same clause; the arc is labeled with a \"\(-\)\" if \(p\) occurs negated. The database is stratified if the graph has no cycle including arcs labeled with a \"\(-\)\". Stratified databases admit a unique \"intended\" minimal model, called the _standard model_[78; 79]. Other minimal models are known, e.g., the _perfect model_ for _locally stratified deductive databases_[80], the _stable model_ semantics [81], and the _well-founded model_ semantics [82]. We adopt the semantics of stratified databases and write \(D\models\phi\), where \(D\) is a database and \(\phi\) a closed formula, to indicate that \(\phi\) holds in \(D\)'s standard model. We now introduce a notation for querying and updating a database. A _query_ is an expression of the form \(\Leftarrow A\), where \(A\) is an atom whose predicate is intensional. When no ambiguity arises, a given query may be indicated directly by means of its _defining formula_ (instead of the predicate name). Definition 2 (Update): An _update_ for an extensional predicate \(p\) in a database \(D\) is an expression of the form \(p(\overrightarrow{X})\Leftarrow p^{\prime}(\overrightarrow{X})\) where \(\Leftarrow p^{\prime}(\overrightarrow{X})\) is a query for \(D\). For an update \(U\), the _updated_ database \(D^{U}\) has the same EDB as \(D\) but in which, for every extensional predicate \(p\) updated as \(p(\overrightarrow{X})\Leftarrow p^{\prime}(\overrightarrow{X})\) in \(U\), the subset \(\{p(\overrightarrow{t})\mid D\models p(\overrightarrow{t})\}\) of EDB is replaced by the set \(\{p(\overrightarrow{t})\mid D\models p^{\prime}(\overrightarrow{t})\}\). Example 1: Consider \(\text{IDB}_{1}=\{p^{\prime}(X)\gets p(X),\quad p^{\prime}(X)\gets X=a\}\). The following update \(U_{1}\) describes the addition of fact \(p(a)\): \(\{p(X)\Leftarrow p^{\prime}(X)\}\). For convenience, wherever possible, defining formulas instead of queries will be written in the body of predicate updates. Update \(U_{1}\) will, e.g., be indicated as follows: \(\{p(X)\Leftarrow p(X)\lor X=a\}\). The constraint verification problem may be formulated as follows. Given a database \(D\), a constraint theory \(\Gamma\) such that \(D\models\Gamma\), and an update \(U\), does \(D^{U}\models\Gamma\) hold too? Since checking directly whether \(D^{U}\models\Gamma\) holds may be too expensive, we aim to obtain a constraint theory \(\Gamma^{U}\), called a _pre-test_, such that \(D^{U}\models\Gamma\) if \(D\models\Gamma^{U}\) and \(\Gamma^{U}\) is easier to evaluate than \(\Gamma\).