  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.
