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.

翻译：开放的两样性被定义为可以显示自由变量的开放过程术语。 洞察力是,为了描述开放的两样性, 我们转向直观模式逻辑的设置。 引入的直观模式逻辑叫做 $\ mathcal{OM}$, 这样的模式在替代模式下封闭, 产生一种被称为直传遗传的属性。 理论遗传遗传学在逻辑中反映了在检查开放的两样性时对自由变量进行的懒惰即时反应。 与我们直观模式逻辑有关的公开两样性的正确性证据在Abella中被机械化。 完整性证据的建设性内容提供了一种算法, 用以生成我们已经实施的区别公式。 我们提请注意一个事实,即存在多种可被直观模式逻辑描述的两样性共性。