Coalgebras, Modal Logic, Stone Duality

代数、模态逻辑、石对偶

• 批准号: EP/C014014/1
• 负责人: Alexander Kurz
• 金额: $ 15.1万
• 依托单位: University of Leicester
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2006
• 资助国家: 英国
• 起止时间: 2006 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FC014014%2F1
• 关键词: Coalgebras; Modal; Logic; Stone; Duality

I.One of the central problems of programming computers is that it isvery difficult to write correct programs or to convince yourself ofthe correctness of some program. One way to tackle this problem is theuse of logic.Let us first take a brief look at logic. We can use logic to (1) make statements about the world, (2) define when a statement holds or does not hold in the world, (3) deduce new statements from given ones using rules of reasoning.`World' can mean the world we live in and logic was originally indeeddeveloped to reason about everyday problems. In mathematics, the worldone reasons about is the world of mathematical objects. Themathematical world is rich enough to model different notions ofcomputation. Mathematical logic thus allows us to devise differentlogics for different models of computation. The logics relevant forthis proposal are known as modal logics.The upshot of this effort should be to make reasoning aboutcomputations completely precise and thus to eliminate the errorshumans tend to make when reasoning about programs.II.In my project I will look at particular models of computation whichare called transition systems. Transition systems consist of statesand relations between states. The idea is that each state representsa given moment of the computation and the relations describe how thecomputation proceeds from on state to another.The project aims at a general theory of logics for transitionsystems. It will establish the relationship between logics andtransition systems via the following detour that allows us to use acertain mathematical theory known as Stone duality. Recent developments suggest using co-algebras to represent transitionsystems. Coalgebras are in a special relationship---calledduality---to algebras. In a similar way as known from solvingequations in school, algebra can be used to formulate reasoningprinciples.In particular, the aims of this proposal are the following. Toassociate to any type of transition system an appropriate logic. Toshow how these logics can be applied to the verification of statementsabout programs. To investigate how certain concepts and tools ofmathematical logic can be adapted to coalgebras and their logics.III.The project will contribute to the theory of coalgebras as a generaltheory of transition systems as developed in the 1990s by manyresearchers. It will also be an important contribution to the recentworks on the connections between (modal) logic andcoalgebras. Coalgebras and modal logic have received attention fromresearchers in different areas of mathematics and computer science andthis research will bring to light new connections them.In a wider context, the project concerns the fundamental relationshipunderlying models of computation on the one hand and logic on theother hand. The development of the theory of coalgebras opens up thepossibility of integrating existing insights and to explore newdirections.

I.编程计算机的主要问题之一是，编写正确的程序或说服您某些程序的正确性是非常困难的。解决这个问题的一种方法是逻辑的使用。让我们首先简要介绍逻辑。我们可以使用逻辑来（1）对世界发表陈述，（2）定义陈述何时成立或不存在于世界，（3）使用推理规则从给定的陈述中推导新陈述。“世界”可以意味着我们生活的世界，逻辑最初确实是为了日常问题而开发的。在数学中，关于世界的原因是数学对象的世界。 theme骨世界足够丰富，可以建模不同的计算概念。因此，数学逻辑使我们能够为不同的计算模型设计不同的logics。相关的逻辑建议被称为模态逻辑。这项工作的结果应该是使对汇票的推理完全精确，从而消除有关programs.ii.ii.ii.i in my项目的propartss.ii.i in My项目时往往会遇到的错误。我将研究所谓的过渡系统的特定计算模型。过渡系统由国家之间的状态和关系组成。这个想法是，每个状态都代表计算的时刻，并且关系描述了该工具如何从状态到另一个状态。它将通过以下弯路建立逻辑和转化系统之间的关系，使我们能够使用称为石头二元性的数学理论。最近的事态发展表明，使用co-elgebras代表过渡系统。煤桥处于特殊关系中 - 称为双重性 - 代数。以与学校的解决方案相似的方式，代数可用于制定推理条件。尤其是，该提案的目的是以下。与任何类型的过渡系统建立联系是适当的逻辑。 Toshow如何将这些逻辑应用于语句验证程序。为了调查某些概念和工具如何适应山地及其逻辑。这也将是对（模态）逻辑和毛金毛之间连接的最近工作的重要贡献。煤炭和模态逻辑已从数学不同领域的研究者和计算机科学领域的研究者中受到关注，这项研究将揭示他们的新联系。在更广泛的背景下，该项目涉及一方面的基本关系在计算的模型和手上的逻辑。煤桥理论的发展开辟了整合现有见解和探索新方向的可能性。

项目成果

Presenting functors on many-sorted varieties and applications

介绍函子的多种分类和应用

• DOI: 10.1016/j.ic.2009.11.007
• 发表时间: 2010
• 期刊: Information and Computation
• 影响因子: 1
• 作者: Kurz A

Functorial Coalgebraic Logic: The Case of Many-sorted Varieties

函子代数逻辑：多分类簇的情况

• DOI: 10.1016/j.entcs.2008.05.025
• 发表时间: 2008
• 期刊: Electronic Notes in Theoretical Computer Science
• 作者: Kurz A

On universal algebra over nominal sets

论名义集合上的通用代数

• DOI: 10.1017/s0960129509990399
• 发表时间: 2010
• 期刊: Mathematical Structures in Computer Science
• 影响因子: 0.5
• 作者: KURZ A

Bitopological duality for distributive lattices and Heyting algebras

• DOI: 10.1017/s0960129509990302
• 发表时间: 2010-01
• 期刊: Mathematical Structures in Computer Science
• 影响因子: 0.5
• 作者: G. Bezhanishvili;N. Bezhanishvili;D. Gabelaia;A. Kurz

Equational Coalgebraic Logic

方程代数逻辑

• DOI: 10.1016/j.entcs.2009.07.097
• 发表时间: 2009
• 期刊: Electronic Notes in Theoretical Computer Science
• 作者: Kurz A