Provenance Analysis for Logic and Games



+49 241 80 21709



The focus of this dissertation project is to apply the concept of provenance analysis which was originally developed for database theory to logic. Provenance analysis aims at determining properties of a database query or in our case a logical formula beyond its truth value. For instance one might be interested in the number of distinct ways one could prove it or maybe we are not convinced of the truth of some input data and would like to know how sure we can be of the result. This can be achieved by interpreting queries or formulae not just as 'true' or 'false' but over a commutative semiring tailored to the additional information we are interested in. If we would like to know the number of distinct proofs, we evaluate over the natural numbers. If we would like to consider different levels of confidence, we will use the so-called Viterbi semiring. This approach has been successfully developed by Green, Karvounarakis and Tannen [1] for different types of positive database languages.

When trying to define provenance analysis for logical formulae using semirings one encounters a problem however. In logic there is negation which is not obviously reproducible in the algebraic context of a semiring. There are several possibilities for treating negation with semiring operations but all have very unintuitive consequences. This unsatisfactory situation was resolved when Grädel and Tannen [2] proposed to treat negation not with a semiring operation but rather by considering the negation normal form of logical formulae and giving semiring values to the literals, not just the positive atoms. These semiring values should be compatible in the sense that the product of the value for a positive atomic formula and the value for its negation should always be zero, corresponding to their conjunction always being false, and their sum should be non-negative, corresponding to their disjunction being (some degree of) true. The values of the literals can then be extended to values for the entire formula by interpreting conjunction and universal quantification as semiring-multiplication and disjunction and existential quantification as semiring-addition. In this way it is possible to evaluate any first-order formula over any commutative semiring.

By evaluating formulae over the semiring N[X] of polynomials with variables in the set X, representing the values of the literals, with coefficients in the natural numbers we obtain the most general provenance analysis possible for positive first-order logic. By this we mean that we obtain a polynomial which allows us to evaluate the formula over any semiring by substituting the semiring-values of the literals for the corresponding variables in the polynomial. This does not account for negation however and therefore only applies to positive first-order logic. To account for negation and to retain the properties for the pairs of atoms and their negations described above, we have to introduce pairs of variables p,p' for atoms and their negations, respectively. If X is the set of these variables we do not consider N[X] but instead we factor out all of the terms p*p', q*q',... meaning that in the factor semiring all these products are zero. This gives us the most general semiring for all of first-order logic.

The aim of this project is to develop similar notions of provenance analysis for logics other than first-order logics, for instance fixed-point logics, guarded logics and verification logics. Similarily we are considering the model-checking games for these logics in order to define a notion of provenance on these games as well as on infinite games in general. Additionally we study the properties of semiring valuations and compare them with the known results for the usual evaluation of formulae as 'true' or 'false'.


[1] T.J. Green, G. Karvounarakis, V. Tannen, "Provenance Semirings", Proceedings of the Twenty-sixth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, p.31-40, 2007

[2] E. Grädel, V. Tannen, "Semiring Provenance for First-Order Model Checking", arXiv:1712.01980, 2017