# Simplified Integrity Checking for an Expressive Class of Denial Constraints
## 3 Relational and Deductive Databases  
In this chapter, we present the basic notation related to deductive databases, and use the syntax of the datalog language as a basis to formulate the main concepts. We refer to standard texts in logic, logic programming, and databases such as [37; 38; 76] for further discussion. As a notational convention, we use lowercase letters to denote _predicates_ (\(p\), \(q\), \(\ldots\)) and _constants_ (\(a\), \(b\), \(\ldots\)) and uppercase letters (\(X\), \(Y\), \(\ldots\)) to denote _variables_. A _term_ is either a variable or a constant; conventionally, terms are also denoted by lowercase letters (\(t\), \(s\), \(\ldots\)) and sequences of terms are indicated by vector notation, e.g., \(\overrightarrow{t}\). The language also includes standard connectives (\(\land\), \(\lor\), \(\
eg\), \(\leftarrow\)), quantifiers, and punctuation. In quantified formulas such as \((\forall XF)\) and \((\exists XF)\), \(X\) is said to be _bound_; a variable not bound is said to be _free_. A formula with no free variables is said to be _closed_. Free variables are indicated in boldface (\(\mathbf{a}\), \(\mathbf{b}\), \(\ldots\)) and referred to as _parameters_; the other variables, unless otherwise stated, are assumed to be universally quantified. Formulas of the form \(p(t_{1},\ldots,t_{n})\) are called _atoms_. An atom preceded by a \(\
eg\) symbol is a _negated atom_; a _literal_ is either an atom or a negated atom. Predicates are divided into three pairwise disjoint sets: _intensional_, _extensional_, and _built-in_ predicates. Intensional and extensional predicates are collectively called _database predicates_; atoms and literals are classified similarly according to their predicate symbol. There is one built-in binary predicate for term equality (\(=\)), written using infix notation; \(t_{1}\
eq t_{2}\) is a shorthand for \(\
eg(t_{1}=t_{2})\) for any two terms \(t_{1}\), \(t_{2}\). A _substitution_\(\{\overrightarrow{X}/\overrightarrow{t}\}\) is a mapping from the variables in \(\overrightarrow{X}\) to the terms in \(\overrightarrow{t}\); its application is the expression arising when each occurrence of a variable in \(\overrightarrow{X}\) is simultaneously replaced by the corresponding term in \(\overrightarrow{t}\). A formula or term which contains no variables is called _ground_. A substitution \(\{\overrightarrow{X}/\overrightarrow{Y}\}\) is called a _renaming_ if \(\overrightarrow{Y}\) is a permutation of \(\overrightarrow{X}\). Formulas \(F\), \(G\) are _variants_ of one another if \(F=G\rho\) for some renaming \(\rho\). A substitution \(\sigma\) is said to be more general than \(\theta\) if there exists a substitution \(\eta\) such that \(\theta=\sigma\eta\). A _unifier_ of \(t_{1},\ldots,t_{n}\) is a substitution \(\sigma\) such that \(t_{1}\sigma=\ldots=t_{n}\sigma\); \(\sigma\) is a _most general unifier_ (mgu) of \(t_{1},\ldots,t_{n}\) if it is more general than any other unifier thereof. A _clause_ is a disjunction of literals \(L_{1}\lor\ldots\lor L_{n}\). In the context of deductive databases, clauses are expressed in implicational form, \(A\gets L_{1}\land\ldots\wedge L_{n}\), where \(A\) is an atom and \(L_{1},\ldots,L_{n}\) are literals; \(A\) is called the _head_ and \(L_{1}\land\ldots\wedge L_{n}\) the _body_ of the clause. The head is optional and, when it is omitted, the clause is called a _denial_. A _rule_ is a clause whose head is intensional, and a _fact_ is a clause whose head is extensional and ground and whose body is empty (understood as _true_). Two clauses are _standardized apart_ if they have no bound variable in common. As customary, we also assume clauses to be _range-restricted_, i.e., each variable must occur in a positive database literal in the body. Deductive databases are characterized by three components: facts, rules, and integrity constraints. An _integrity constraint_ can, in general, be any (closed) formula.