Abstract
Provenance analysis is used to track the provenance or dependence of computed facts from different input items, via interpretations in commutative semirings.
In joint work with Val Tannen, done during the Logical Structures in Computation Programme at the Simons Institute, we have generalized this approach from the traditional setting of positive query languages, such as positive relational algebra and datalog, to logics that include negation, such as full FO and LFP. This is actually closely connected to the study of finite and infinite games. Indeed, one can see the provenance interpretation of a logical formula on a given finite structure as a semiring evaluation of the associated model checking game.
Further, provenance analysis provides interesting insights on games to answer more subtle questions than just who wins the game, such the number or costs of winning strategies, or issues such as confidence and trust in game-theoretic settings. Further, for modal and guarded logics, a provenance analysis through their natural model checking games may provide more adequate results than through their standard translations into FO or LFP.