In the present paper, we develop the algorithmic correspondence theory for hybrid logic with binder. We define the class of Sahlqvist inequalities, each inequality of which is shown to have a first-order frame correspondent effectively computable by an algorithm ALBA.
翻译:在本文中,我们发展了混合逻辑和粘合器的算法对应理论。 我们定义了Sahlqvist不平等的类别,其中的每一种不平等都显示有一个由ALBA算法有效计算的第一阶框架通讯员。