Coalgebra-based generic decision procedures and complexity bounds for modal and hybrid logics

模式逻辑和基本模式语言的各种扩展，例如提供关于个体的推理的表达手段的混合语言和捕捉不同形式的时间发展的定点语言，传统上在计算机科学中扮演着中心角色，特别是在反应系统的分析和知识表示中。在这两个领域，都有一种明显的趋势，即超越经典的克里普克式的对模式的关系解释，转向更复杂的系统类型，例如基于游戏的、概率的或优先的系统，从而产生例如交替时间的时态逻辑、概率描述逻辑和非单调的条件逻辑，它们遵循与关系模式逻辑相当不同的规律。余代数逻辑提供了一个框架，在该框架中，可以以语义统一的方式处理各种各样的这样的逻辑，并且实际上甚至允许开发通用算法和随后的通用复杂性分析。本课题旨在进一步扩展和深化余代数模态逻辑的算法基础，特别是针对迭代逻辑、不动点逻辑、一阶余代数逻辑的可判定片段以及多维余代数逻辑。通用算法将与一系列通用启发式优化策略相结合，以获得用于协代数、时序和描述逻辑的高效推理器。

Modal logics and various extensions of the basic modal language, e.g. hybrid languages that provide expressive means for reasoning about individuals and fixed point languages that capture different forms of temporal development, traditionally play a central role in computer science, in particular in the analysis of reactive systems and in knowledge representation. In both areas, there has been a notable tendency to move beyond the classical Kripke-style relational interpretation of modalities towards more elaborate system types, such as game-based, probabilistic, or preferential systems, giving rise, e.g., to alternating-time temporal logic, probabilistic description logics, and non-monotonic conditional logics, which obey rather different laws than relational modal logics. Coalgebraic logic provides a framework in which a wide variety of such logics can be treated in a semantically uniform manner, and indeed even allows for the development of generic algorithms and an ensuing generic complexity analysis. The current project is aimed at further extending and deepening the algorithmic foundations of coalgebraic modal logic, in particular towards iterative logics, fixed point logics, decidable fragments of coalgebraic first-order logics, and many-dimensional coalgebraic logics. The generic algorithms will be combined with a range of generic heuristic optimization strategies to obtain an efficient reasoner for coalgebraic temporal and description logics.