Provenance Analysis for Logic and Games

sentence is true in a given finite structure. Provenance analysis,
based on interpretations in commutative semirings, abstracts
from such a computation mathematical information on how the result
depends on the atomic data that describe the structure.

In this approach, atomic facts are interpreted not just by true
or false, but by values in an appropriate semiring, where 0 is
the value of false statements, whereas any element $a\neq 0$ of the
semiring stands for some shade of truth. These values are then
propagated from the atomic facts to arbitrary statements in the language.

In database theory, provenance analysis has been successfully developed
for positive query languages such a unions of conjunctive queries,
positive relational algebra, or datalog. However, it did not really
offer an adequate treatment of negation or missing information.


We propose a new approach for the provenance analysis of logics with
negation, such as first-order logic and fixed-point logics. It is
closely related to a provenance analysis of the associated model-checking
games, and based on new provenance semirings of polynomials and formal
power series, which take negation into account. They are obtained by
taking quotients of traditional provenance semirings by congruences
generated by products of positive and negative provenance tokens;
they are called semirings of dual-indeterminate polynomials or
dual-indeterminate power series.


Beyond the use for model-checking problems in logics, provenance
analysis of games is of independent interest. Provenance values in
games provide detailed information about the number and properties
of the strategies of the players, far beyond the question whether
or not a player has a winning strategy from a given position.


This is joint work with Val Tannen.