Towards constraint provenance games

Provenance for positive queries is well understood and elegantly handled by provenance semirings [GKT07], which subsume many earlier approaches. However, the semiring approach does not extend easily to why-not provenance or, more generally, first-order queries with negation. An alternative approach is to view query evaluation as a game between two players who argue whether, for given database I and query Q, a tuple t is in the answer Q(I) or not. For first-order logic, the resulting provenance games [KLZ13] yield a new provenance model that coincides with provenance semirings (how provenance) on positive queries, but also is applicable to first-order queries with negation, thus providing an elegant, uniform treatment of earlier approaches, including why-not provenance and negation. In order to obtain a finite answer to a why-not question, provenance games employ an active domain semantics and enumerate tuples that contribute to failed derivations, resulting in a domain dependent formalism. In this paper, we propose constraint provenance games as a means to address this issue. The key idea is to represent infinite answers (e.g., to why-not questions) by finite constraints, i.e., equalities and disequalities.