© 1988 by British Computer Society
A Top-down Inference Procedure for Template Dependencies

1 Department of Electrical Engineering and Computer Science, Northwestern University, Evanston, IL 60201, USA, 2 Department of Computer Science Engineering, The University of Texas at Arlington, P.O. Box 19015, Arlington, TX 76019, USA
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 know 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.
Received June 1986.
* Department of Electrical Engineering and Computer Science, Northwestern University, Evanston, IL 60201, USA
Department of Computer Science Engineering, The University of Texas at Arlington, P.O. Box 19015, Arlington, TX 76019, USA