Provenance Analysis for Logic and Games

逻辑和游戏的起源分析

• 批准号: 434376062
• 负责人: Professor Dr. Erich Grädel
• 金额: --
• 依托单位: Informatik 7: Lehr- und Forschungsgebiet für Mathematische Grundlagen der Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/434376062?language=en
• 关键词: Provenance; Analysis; Logic; Games

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.

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