Resolution with order and selection for hybrid logics (Q2429982)

In the paper the labeled resolution calculus for hybrid logics is presented. The authors show that the general framework of saturation-based reasoning for first-order logic with equality can be adapted to calculi for other logics. They show then that the calculus presented is complete for any admissible order and selection function. It gives a decision method for some fragment of hybrid logic. Since hybrid logics are extensions of modal logics, the results of the paper can also be applied to a number of modal logics.