Towards Constraint Provenance Games

Provenance for positive queries is well understood and elegantly handled by provenance semirings, 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 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.