Coalgebraic Logic: Expanding the Scope

点击翻译按钮获取中文摘要

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)