LIRa session (online only): Erich Grädel

Date and Time: Thursday, October 29th 2020, 16:30-18:00, Amsterdam time.

Venue: online.

Title: Semiring Provenance for Logic and Games


Semiring provenance is a successful approach, originating in database theory, to providing detailed information on how atomic facts in a given finite structure combine to yield the truth or falsity of a logical statement. In particular, general provenance semirings of polynomials or formal power series provide precise descriptions of the evaluation strategies or “proof trees” for the statement. By evaluating these descriptions in specific application semirings, one can extract practical information for instance about the confidence that we assign to a statement or about the cost of its evaluation.

While semiring provenance, as developed in database theory, has mainly been confined to positive query languages, such as (unions of) conjunctive queries, positive relational algebra, or datalog, we generalize this approach to logics that include negation, such as full first-order logic or least fixed-point logic, exploiting connections between logic and games. Specific mathematical challenges arise from the interleaving of negation and fixed-point inductions, which lead us to the study of fully continuous absorptive semirings and to generalized absorptive polynomials.

Beyond the applications to the evaluation of database query and logical sentences, semiring provenance also has interesting interpretations in finite and infinite games. Semiring evaluations permit 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 cost in game-theoretic settings.