A Proof Procedure for Data Dependencies

Abstract

A class of dependencies, tuple and equality generating dependencies, is defined, and the chase process is generalized to deal with these dependenetes. For total dependencies the chase is an exponential ttme decision procedure for the implication problem, and in some restricted cases it can be modified to run m polynomial Ume. For nontotal dependencies the chase is only a proof procedure. However, several cases for which it is a decision procedure are shown. It is also shown that equality is redundant for deciding implication of tuple-generating dependencies, and is “almost redundant” for deciding implication of equality-generating dependencies. © 1984, ACM. All rights reserved.