Exploiting Equality Generating Dependencies in Checking Chase Termination

The chase is a well-known algorithm with a wide range ofapplications in data exchange, data cleaning, data integration, query optimization, and ontological reasoning. Sincethe chase evaluation might not terminate and it is undecidable whether it terminates, the problem of defining (decidable) sufficient conditions ensuring termination has receiveda great deal of interest in recent years. In this regard, severaltermination criteria have been proposed. One of the mainweaknesses of current approaches is the limited analysis theyperform onequality generating dependencies(EGDs).In this paper, we propose sufficient conditions ensuringthat a set of dependencies has at least one terminating chasesequence. We propose novel criteria which are able to perform a more accurate analysis of EGDs. Specifically, wepropose a new stratification criterion and an adornment algorithm. The latter can both be used as a termination criterion and be combined with current techniques to make themmore effective, in that strictly more sets of dependencies areidentified. Our techniques identify sets of dependencies thatare not recognized by any of the current criteria.