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.