Editing Hybrid logic (section)

'''Hybrid logic''' refers to a number of extensions to [[propositional logic|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 complexity|computational tractability]]. The history of hybrid logic began with [[Arthur Prior]]'s work in [[tense logic]].<ref>{{cite encyclopedia |url=http://plato.stanford.edu/entries/logic-hybrid/ |title=Hybrid Logic |author=Torben Braüner |date=2008 |encyclopedia=[[Stanford Encyclopedia of Philosophy]] |accessdate=1 February 2011}}</ref>

Unlike ordinary modal logic, hybrid logic makes it possible to refer to states (possible worlds) in [[formula (logic)|formula]]s.

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:

:''@<sub>i</sub> p'' is true [[iff|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 logic]]s (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 [[Abox|TBox]] reasoning.