Algorithmic Correspondence for Hybrid Logic with Binder

TL;DR

This paper extends algorithmic correspondence theory to hybrid logic with binder, introducing a class of inequalities that can be effectively translated into first-order frame conditions using the ALBA algorithm.

Contribution

It develops the first algorithmic approach for correspondence in hybrid logic with binder, defining Sahlqvist inequalities and enabling effective computation of frame correspondents.

Findings

Defined Sahlqvist inequalities for hybrid logic with binder

Developed an effective algorithm ALBA for correspondence computation

Established first-order frame correspondents for the inequalities

Abstract

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.