Equality-generating dependency

In relational database theory, an equality-generating dependency is a certain kind of constraint on data. It is a subclass of the class of embedded dependencies.
An algorithm known as the chase takes as input an instance that may or may not satisfy a set of EGDs, and, if it terminates, output an instance that does satisfy the EGDs.
An important subclass of equality-generating dependencies are functional dependencies.

Definition

An equality-generating dependency is a sentence in first-order logic of the form:
where, is a conjunction of relational and equality atoms and is a non-empty conjunction of equality atoms. A relational atom has the form and an equality atom has the form, where each of the terms are variables or constants.
Actually, one can remove all equality atoms from the body of the dependency without loss of generality. For instance, if the body consists in the conjunction, then it can be replaced with .
An equivalent definition is the following:
where.
Indeed, generating a conjunction of equalities is equivalent to have multiple dependencies which generate only one equality.