All-Instances Termination of Chase is Undecidable

We show that all-instances termination of chase is undecidable. More precisely, there is no algorithm deciding, for a given set T consisting of Tuple Generating Dependencies (a.k.a. Datalog. program), whether the T-chase on D will terminate for every finite database instance D. Our method applies to Oblivious Chase, Semi-Oblivious Chase and - after a slight modification - also for Standard Chase. This means that we give a (negative) solution to the all-instances termination problem for all version of chase that are usually considered. The arity we need for our undecidability proof is three. We also show that the problem is EXPSPACE-hard for binary signatures, but decidability for this case is left open. Both the proofs - for ternary and binary signatures - are easy. Once you know them.