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 (how easy it is to compute/reason with logical languages). 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 (possible worlds) 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:

@_i p is true if and only if p is true in the unique state named by the nominal i (i.e., the state where i is true).

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 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. 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.