Provenance Analysis for Logic and Games

起源分析和语义学基于这样一种想法，即不仅根据真或假来评估逻辑语句，而且还根据某些交换半环中的值来评估逻辑语句。在这种情况下，当使用布尔半环时，经典语义学再次出现作为特例。其他半环提供额外的信息，例如用于成本计算、用于计算评估策略和证据、用于访问级别和安全问题等。此外，多项式的起源半环或形式幂理论，具有代数意义上的普遍性质，被用来寻找最一般的起源估值。特别是，它们承认跟踪原子事实，并提供准确的见解，哪些原子事实组合产生逻辑陈述的真实性，以及这些组合在成功的评估中使用的频率。对于正向数据库查询语言，语义起源已经成功应用了15年以上。这个研究项目的目标是系统地将起源分析和语义扩展到与计算机科学的各个领域相关的广泛的逻辑形式主义，以及有限和无限游戏的类别。这也为来源分析的新应用打开了大门。这个项目的重要出发点是我们处理具有对偶不定的多项式半环中的否定的新方法，以及起源分析与有限和无限对策理论的联系。在该项目的第一阶段，在实现这些目标方面取得了重大进展。现在更好地理解了半环语义学的代数、逻辑和博弈论基础。确定了适用于定点计算的半环，并为具有最小和最大不动点的否定和交织的一般不动点逻辑找到了适当的半环语义，包括算法评估策略和相关的模型检验博弈。可以回答半环语义学的重要模型论问题。起源分析也被确立为一种新的游戏策略分析方法。策略和定理已被证明适用于许多不同的博弈模型，并通过对Büchi博弈的详细案例分析说明了该方法的意义和价值。在这个项目的第二阶段，我们希望在几个方向上扩展和深化我们的成果，并弥合理论上的剩余差距。这包括逻辑、算法和博弈论方面，以及应用程序，例如修复丢失或不准确的数据，以及逻辑学习理论。我们的目标是使起源分析和语义学成为计算机科学中一个成熟的逻辑领域。

Provenance analysis and semiring semantics are based on the idea to evaluate logical statements not just by true or false, but by values in some commutative semiring. In this context, the classical semantics re-appears as the special case, when the Boolean semiring is used. Other semirings provide additional information, for instance for cost computations, for the counting of evaluation strategies and proofs, for access levels and security issues, and so on. Further, provenance semirings of polynomials or formal power theories, with universal properties in an algebraic sense, are used to find most general provenance valuations. In particular, they admit the tracking of atomic facts, and give precise insights which combinations of atomic facts yield the truth of a logical statement, and how often these are used in a successful evaluation. For positive database query languages, semiring provenance has been successfully applied for more than 15 years. The objective of this research project is the systematic extension of provenance analysis and semiring semantics to a broad spectrum of logical formalisms which are relevant in various areas of computer science, and as well to classes of finite and infinite games. This also opens the door to new applications of provenance analysis. Important starting points of this project have been our new approach for the treatment of negation in polynomial semirings with dual indeterminate, and the connections of provenance analysis to the theory of finite and infinite games. Tn the first phase of this project, significant progress towards these objectives has been made. Algebraic, logical, and game-theoretic foundations of semiring semantics are now much better understood. Suitable semirings for fixed-point computations have been identified, and an adequate semiring semantics for general fixed-point logics with negation and interleaving of least and greatest fixed points has been found, including algorithmic evaluation strategies and associated model-checking games. Important model-theoretic questions of semiring semantics could be answered. Provenance analysis has also been established as a new method for the strategy analysis in games. Sum-of-Strategies-Theorems have been proved for a number of different game models, and the significance and value of this method has been illustrated by a detailed case analysis for Büchi games. In the second phase of this project, we want to extend and deepen our results in several directions, and close remaining gaps in the theory. This includes logical, algorithmic, and game-theoretic aspects, as well as applications, for instance for repairs of missing or inaccurate data, and logical learning theory. Our goal is to make provenance analysis and semiring semantics a mature field of logic in computer science.