Many-sorted hybrid modal languages

We continue our investigation into using the hybridization technique on top of the many-sorted polyadic modal logic we have previously defined. By adding different operators and binders, we present in this paper several systems we have developed. We briefly discuss the goals we have achieved by developing each system. We identify a fragment of the full hybrid logic, for which we prove its sound and complete deduction and we show that it is powerful enough to represent both the programs and their semantics in an uniform manner. Finally, we provide a standard translation from full hybrid many-sorted logic to first-order logic.