一句话：提出直觉主义模态逻辑 OM 刻画开放互模拟，并从完备性证明提取区分公式生成算法。
开放互模拟定义在可能含有自由变量的开放进程项上，为其寻找逻辑刻画较为困难。本文转向直觉主义模态逻辑，提出逻辑 OM，其模态算子对替换封闭，从而具有“直觉主义遗传性”，在逻辑层面反映检查开放互模拟时对自由变量的惰性实例化。作者在 Abella 中机器化验证了开放互模拟相对于 OM 的可靠性；完备性证明的构造性内容给出生成区分公式的算法，并已实现。论文还指出，存在一族可由直觉主义模态逻辑刻画的互模拟同余关系。
Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are closed under substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic hereditary reflects in logic the lazy instantiation of free variables performed when checking open bisimilarity. The soundness proof for open bisimilarity with respect to our intuitionistic modal logic is mechanised in Abella. The constructive content of the completeness proof provides an algorithm for generating distinguishing formulae, which we have implemented. We draw attention to the fact that there is a spectrum of bisimilarity congruences that can be characterised by intuitionistic modal logics.
@article{paperbot1287,
title = {A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic},
author = {Ki Yung Ahn and Ross Horne and Alwen Tiu},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:2)2021}
}