Hybrid logic

From Wikipedia, the free encyclopedia

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

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:

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