一句话：为局部单调内函子上的 T-余代数提出有限化 Moss 覆盖模态逻辑，建立基概念并证明 Hennessy-Milner 性质与序列演算完备性。
本文为局部单调内函子 T 上的 T-余代数给出有限化 Moss 余代数逻辑。该逻辑仅含一个覆盖模态，其元数由 T 的对偶 T_ω^∂ 的最小有限子函子决定，语义通过关系提升解释。为使语义成立，要求 T 保持精确方形；为使有限化成立，要求 T_ω^∂ 保持有限交。作者在带合适分解系统的范畴中一般地引入子对象基概念，用于讨论给定公式的有限子公式偏序集。进一步证明该逻辑相对于基于关系提升的相似性具有 Hennessy-Milner 性质，并定义序列证明系统且证明其完备性。
We present a finitary version of Moss' coalgebraic logic for $T$-coalgebras, where $T$ is a locally monotone endofunctor of the category of posets and monotone maps. The logic uses a single cover modality whose arity is given by the least finitary subfunctor of the dual of the coalgebra functor $T_\omega^\partial$, and the semantics of the modality is given by relation lifting. For the semantics to work, $T$ is required to preserve exact squares. For the finitary setting to work, $T_\omega^\partial$ is required to preserve finite intersections. We develop a notion of a base for subobjects of $T_\omega X$. This in particular allows us to talk about the finite poset of subformulas for a given formula. The notion of a base is introduced generally for a category equipped with a suitable factorisation system. We prove that the resulting logic has the Hennessy-Milner property for the notion of similarity based on the notion of relation lifting. We define a sequent proof system for the logic, and prove its completeness.