权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Fixed point logics: expressive power, structure, complexity

定点逻辑：表达能力、结构、复杂性

基本信息

批准号：
199814663
负责人：
Professor Dr. Erich Grädel
金额：
--
依托单位：
Informatik 7: Lehr- und Forschungsgebiet für Mathematische Grundlagen der Informatik
依托单位国家：
德国
项目类别：
Research Grants
财政年份：
2011
资助国家：
德国
起止时间：
2010-12-31 至 2017-12-31
项目状态：
已结题

来源：
https://gepris.dfg.de/gepris/projekt/199814663?language=en
关键词：
Fixed point logics expressive power

项目摘要

Fixed point logics play a central role in many areas of mathematical logic and its applications in computer science. In this project we investigate fixed point logics in the context of the quest for a logic for polynomial time and the definability of algorithmic problems in (linear) algebra, in connection with bisimulation safety on transition systems and extensions of modal logics, as well as in the context of the theory of infinite games.The central challenge in finite model theory is the quest for a logic for polynomial time. The study of different kinds of fixed point logics has led to logical characterizations of more and more powerful fragments of polynomial time. On the other hand one has isolated a number of fundamental algorithmic methods that cannot be expressed in classical fixed point logics. These include algorithmic techniques from (linear) algebra, from graph theory (e.g. concerning graph isomorphism) and for parallel computation. In this project we extend fixed point logics by such algorithmic methods and investigate their complexity, expressive power, and structure.In addition we intend to give a new impulse to the field of modal logics bythe construction and analysis of modal logics that go beyond state formulae and monadic fixed points, but guarantee safety under bisimulations. We will use these and other approaches to strengthen our understanding of the connection between fixed point logics and infinite games, especially concerning the definability of winning strategies. Finally we investigate the relationship of fixed point logics with a relatively new family of logics for reasoning about dependence, independence, and imperfect information, on the basis of Hodges' team semantics.

不动点逻辑在数理逻辑的许多领域及其在计算机科学中的应用中起着核心作用。在这个项目中，我们研究不动点逻辑的背景下，寻求一个逻辑的多项式时间和算法问题的可定义性（线性）代数，与互模拟安全的过渡系统和扩展的模态逻辑，以及在理论的背景下的无限games.The中心的挑战，在有限模型理论是寻求一个逻辑的多项式时间。对不同类型的不动点逻辑的研究导致了越来越多的强大的多项式时间片段的逻辑刻画。另一方面，人们已经孤立了一些基本的算法方法，不能在经典的不动点逻辑表示。这些包括算法技术从（线性）代数，从图论（例如，关于图同构）和并行计算。在这个项目中，我们用这些算法方法扩展了不动点逻辑，并研究了它们的复杂性、表达能力和结构，另外，我们打算通过构造和分析超越状态公式和一元不动点，但在互模拟下保证安全的模态逻辑，给模态逻辑领域带来新的推动。我们将使用这些方法和其他方法来加强我们对不动点逻辑和无限博弈之间联系的理解，特别是关于获胜策略的可定义性。最后，我们调查的关系不动点逻辑与一个相对较新的家庭的逻辑推理的依赖，独立性和不完美的信息，霍奇斯的团队语义的基础上。