Non-Uniformly Terminating Chase: Size and Complexity

TL;DR

This paper investigates the non-uniform termination and size bounds of the semi-oblivious chase procedure for guarded TGDs, demonstrating polynomial-time termination checks and linear size results.

Contribution

It establishes that non-uniform semi-oblivious chase termination for guarded TGDs can be decided in polynomial time and the chase result size is linear, extending techniques from query answering.

Findings

Non-uniform chase termination is polynomial-time decidable.

Chase result size is linear in the database when finite.

Techniques like simplification and linearization are applicable to chase termination.

Abstract

The chase procedure, originally introduced for checking implication of database constraints, and later on used for computing data exchange solutions, has recently become a central algorithmic tool in rule-based ontological reasoning. In this context, a key problem is non-uniform chase termination: does the chase of a database w.r.t. a rule-based ontology terminate? And if this is the case, what is the size of the result of the chase? We focus on guarded tuple-generating dependencies (TGDs), which form a robust rule-based ontology language, and study the above central questions for the semi-oblivious version of the chase. One of our main findings is that non-uniform semi-oblivious chase termination for guarded TGDs is feasible in polynomial time w.r.t. the database, and the size of the result of the chase (whenever is finite) is linear w.r.t. the database. Towards our results concerning non-uniform chase termination, we show that basic techniques such as simplification and linearization, originally introduced in the context of ontological query answering, can be safely applied to the chase termination problem.