In formal logic, there is a trade-off between expressiveness and computational tractability.
This is achieved by a class of formulas called nominals, which are true in exactly one state, and by the use of the @ operator, which is defined as follows: Hybrid logics with extra or other operators exist, but @ is more-or-less standard.
Hybrid logics have many features in common with temporal logics (which sometimes use nominal-like constructs to denote specific points in time), and they are a rich source of ideas for researchers in modern modal logic.
They also have applications in the areas of feature logic, model theory, proof theory, and the logical analysis of natural language.
Hybrid logic is also closely connected to description logic because the use of nominals allows one to perform assertional ABox reasoning, as well as the more standard terminological TBox reasoning.