We investigate intuitionistic modal logics with locally interpreted $\square$ and $\lozenge$. The basic logic LIK is stronger than constructive modal logic WK and incomparable with intuitionistic modal logic IK. We propose an axiomatization of LIK and some of its extensions. We propose bi-nested calculi for LIK and these extensions, thus providing both a decision procedure and a procedure of finite countermodel extraction.

翻译：我们研究了具有局部解释的$\square$和$\lozenge$的直觉模态逻辑。基本逻辑LIK强于构造性模态逻辑WK，且与直觉模态逻辑IK不可比较。我们提出了LIX及其若干扩展的公理化系统，并为LIK及这些扩展设计了双嵌套演算，从而同时提供了判定过程与有限反模型提取过程。