Equality generating dependency

In relational database theory, an equality-generating dependency (EGD) is a certain kind of constraint on data. It is a subclass of the class of embedded dependencies (ED). An ED is a sentence in first-order logic of the form: ∀x1 ... xn, P(x1, ..., xn) → ∃z1, ..., zk, Q(y1, ..., ym) where {z1, ..., zk} = {y1, ..., ym} \ {x1, ..., xn}, and P is a possibly empty and Q is a non-empty conjunction of equality atoms. A n equality atom has the form wi = wj where each of the w, ..., wh, wi, wj, are variables or constants. An algorithm known as the chase takes as input an instance that may or may not satisfy a set of EGDs (or more generally a set of EDs), and, if it terminates (which is a priori undecidable), output an instance that does satisfy the EGDs.