Hybrid logic
Hybrid logic refers to a number of extensions to propositional modal logic with more expressive power, though still less than first-order logic. In formal logic, there is a trade-off between expressiveness and computational tractability. The history of hybrid logic began with Arthur Prior's work in tense logic.
Unlike ordinary modal logic, hybrid logic makes it possible to refer to states in formulas.
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, 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. It is also deeply 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.
