The chase procedure, for determining if a given dependency must hold in any relation where a set of dependencies is known to hold, operates bottom-up by constructing a hypothetical relation known as a tableau. A top-down counterpart, based on resolution theorem proving techniques, is introduced in which, through factoring, resolvents which contain function terms may be avoided. A literal numbering technique, which limits the number of resolvents, is also examined.
ASJC Scopus subject areas
- General Computer Science