有序余代数的莫斯逻辑
摘要：具有有限性的认同逻辑在T-代数中呈现出来，其中T是一种局部单调的偏序集类别和单调映射的函子。该逻辑使用一个由余代数函子T_ω^partial的对偶形式的最小有限子函子确定的单覆盖模态，并且模态的语义是由关系提升给出的。为了使语义有效，要求T保持精确的正方形。为了使有限设定起作用，要求T_ω^partial保持有限交集。我们提出了一个T_ωX的子对象基的概念。这特别允许我们讨论给定公式的子公式的有限偏序集。基础概念通常被引入到具有适当因子化系统的类别中。我们证明了所得到的逻辑在基于关系提升的相似性概念上具有Hennessy-Milner性质。我们为该逻辑定义了一个顺推证明系统，并证明了其完备性。
作者：Marta B''ilkov''a, Matv{e}j Dost''al
论文ID：1901.06547
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22