Coalgebraic Logic: Expanding the Scope

COALGEBRAIC LOGICLOGIC在计算机科学中起着基础性作用。在最基本的层面上，布尔逻辑被用来设计我们每天在计算机中使用的电路。在较高端，计算机执行的任务需要符合以适合程序员、分析员甚至其他计算设备的逻辑表示的规范。这样的规范逻辑必须能够表达许多不同的概念，如时间、知识、空间、流动性、通信、概率、条件等。为这些概念中的每一个定制逻辑，并在模态逻辑的保护伞下进行研究。在将模态逻辑用于系统规范的任何实质性应用中，都会出现组合不同逻辑的需要，每个逻辑都考虑到上述方面之一。并不是所有的逻辑都有标准的Kriske语义，但在所有情况下，语义都可以被认为是余代数的。余代数将模态逻辑的标准Klipke语义推广到邻域框架、马尔可夫链、拓扑空间等概念，而且余代数是范畴理论中的一个概念。范畴理论是一个数学领域，它用抽象的术语描述数学结构，使这些结构适用于数学、逻辑和计算机科学的许多不同领域。特别地，余代数的范畴理论性质允许我们使用范畴理论构造来处理模性问题。范畴理论的优点之一是，由于它们的普遍性，这些结构适用于特定语言及其语义模型。总而言之，余代数逻辑结合了模态逻辑和余代数。这将模态逻辑从Klipke框架推广到余代数，并使范畴理论方法和构造在模态逻辑中可用。对SCOPE余代数逻辑的解释可以追溯到1997年，当时Moss的同名论文的第一稿被传阅。从那时起，许多研究人员已经开发出了它。就在刚才，余代数逻辑即将确立自己的一个领域。虽然目前余代数逻辑的许多工作都是为了利用当前的成果以获得更多的应用，但这个项目是从以下两个方面开始的：第一，余代数逻辑还没有利用模态逻辑中的许多重要发展。其中两个发展是：1)模态逻辑和一阶逻辑之间的关系；2)对模态逻辑类的统一处理。第二，模态逻辑和论域理论有许多平行的发展。其中一些关系直到最近才变得清晰起来，因为这两个领域都有余代数的联系。因此，我们计划从模态逻辑中推广方法，以便它们可以应用于领域理论中产生的逻辑(这将包括在上面1和2项下完成的工作)

COALGEBRAIC LOGICLogic plays a fundamental role in Computer Science. At the most basiclevel, Boolean logic is used to design the circuits we use every day inour computers. At the higher end, the tasks that computers perform need toconform to specifications expressed in logics suitable for programmers,analysts or even other computational devices.Such specification logics have to be able to express many differentconcepts such as time, knowledge, space, mobility, communication,probability, conditionals etc. Bespoke logics for each of these conceptsexist and are studied under the umbrella of Modal Logic.In any substantial application of Modal Logic to the specification ofa system, the need to combine different logics will arise, each logicaccounting for, eg, one of the aspects mentioned above. The need thenarises to deal with these logics in a uniform and modular way.Not all of these logics have a standard Kripke semantics, but in allcases, the semantics can be considered to be coalgebraic. Coalgebrasgeneralise the standard Kripke semantics of modal logic to encompassnotions such as neighbourhood frames, Markov chains, topologicalspaces, etc.Moreover, Coalgebra is a concept from Category Theory. Category Theoryis an area of mathematics which describes mathematical constructionsin abstract terms that make these constructions available to manydifferent areas of mathematics, logic, and computer science. Inparticular, the category theoretic nature of Coalgebras allows us totackle the modularity problem using category theoreticconstructions. One of the benefits of category theory is that theseconstructions, because of their generality, apply to specificationlanguages and to their semantic models.To summarise, Coalgebraic Logic combines Modal Logic withCoalgebra. This generalises modal logics from Kripke frames tocoalgebras and makes category theoretic methods and constructionsavailable in Modal Logic.EXPANDING THE SCOPECoalgebraic Logic can be traced back to 1997 when the first draft ofMoss's paper with the same title was circulated. Since then, it hasbeen developed by a number of researchers. Just now, Coalgebraic Logicis about to establish itself as an own area. Whereas much of thecurrent work in Coalgebraic Logic aims at exploiting the currentachievements towards more applications, this project starts from thefollowing two observations:First, Coalgebraic logic did not yet make use of many of the importantdevelopments that have taken place in Modal Logic. Two of thesedevelopments are:1) the relationship between Modal Logic and First-Order Logic and2) the uniform treatment of classes of modal logics.Second, there exist many parallel developments in Modal Logic andDomain Theory. Some of the relationships have only recently becomeclear, through the connection of both areas with Coalgebra. Wetherefore plan to3) generalise methods from Modal Logic so that they can be applied tothe logics arising in Domain Theory (this will include the work doneunder 1 and 2 above)