# Hybrid Logics in Action

Modal logicians like to point out that many of the formalisms
invented by researchers in artificial intelligence, computational
linguistics, and other fields are actually notational variants of
modal logic. But in many cases it would be more accurate to say that
it is *hybrid logics* which are reinvented in this way.
Moreover, it is arguable that when it comes to providing usable proof
systems, hybrid languages are more natural than orthodox modal logics.
Let's take a closer look at these claims.

#### Description Logic

It is well known that the description language , see [Schmidt-Schauss and Smolka 1991], is a notational variant of multi-modal logic, see [Schild 1991]. But this relation only ho lds at the level of T-Box reasoning (that is, general reasoning about concepts). It is often important to perform A-Box (or assertional) reasoning as well -- that is, to reason about how concepts apply to particular individuals. Cutting a long (and interesting) story short, A-Box reasoning corresponds to a restricted use of operators, while the ``one-of'' operators used in some versions of description logic are essentially disjunctions of nominals; see [Blackburn and Tzakova 1998,Areces and de Rijke 1999]. Now, A-Box reasoning plays a central role in description logic, thus to claim that description logic is simply modal logic is an oversimplification. A-Box reasoning introduces ideas that aren't present in orthodox modal logic; concepts from hybrid logic are needed to complete the picture. The connection between hybrid logics and description logics has also been explored by the description logic community; see, for example, [De Giacomo 1995].

#### Feature Logic

In a similar vein, the Attribute Value Matrices (AVMs) used in
computational linguistics are an obvious notational variant of
deterministic multi-modal logic -- at least, if you ignore the
``tags'' which are used to indicate re-entrancy of feature structues.
But to ignore re-entrancy is to ignore the fundamental mechanisms
underlying PATR-II and many other unification-based approaches to
grammar. And it is *easy* to account for re-entrancy in the
setting of hybrid logic: ``tags'' are simply nominals. Incidentally,
if you're familiar with feature logic, it's worth knowing that the
hybrid approach to feature logic differs from that taken in
Kasper-Rounds logic in a number of respects. Kasper-Rounds logic is
essentially a fragment of deterministic Propositional Dynamic Logic
with intersection. It encodes re-entrancy in a different way, and has
very different model-theoretic and complexity-theoretic properties.
For more information, see [Blackburn 1993a], [Blackburn and Spaan 1993], and
[Reape 1994].

#### Indexicality and Multidimensional Logic

Hybrid languages are also a natural resource for studying indexicality
in natural language. The classical tool for this purpose is
*multidimensional modal logic*. In these systems, formulas are
evaluated at sequences of points, and the basic idea is that one point
of the sequence is thought of as the point of evaluation, while the
others are used as memory locations to store references like `now',
`then', etc. Key references in this tradition include
[Kamp 1971], [Vlach 1973], and [Gabbay 1976].
However with the exception of [Cresswell 1990] and
[Cresswell 1996], there seems to have
been relatively little work on
such approaches recently.

Hybrid languages offer a novel perspective from which to re-assess,
and unify, the work in this tradition. Hybrid languages move
multidimensional logic's sequence of evaluation points from the
metalanguage to the object language, with hybrid variables acting as
names for indices. Moreover, when equipped with the
operator, hybrid languages offer the `de-scoping' behavior typic
al of
such multidimensional operators as **Now** and **Then**.

There are also links between hybrid logic and mathematical aspects of multidimensional modal logic tradition (particularly the multidimensional perspective on cylindric algebra; see [Marx and Venema 1997]). As is shown in [Areces, Blackburn and Marx 1998], can be viewed as an explicit substitution device, providing a different perspective on cylindrification.

#### Modal Logics of Information Systems

Nominals have turned up in yet another setting, namely the Polish tradition of modal logics for information systems initiated by Eva Orlowska (see, for example, [Orlowska (ed.)1997]). Themes in this tradition include the development of modal logics of similarity (or relative similarity) and there are strong links with the tradition of rough-set theory. In a series of papers, Beata Konikowska has introduced nominals to such logics; see [Konikowska 1997a], [Konikowska 1987], and [Konikowska 1997b]. Intriguingly, u nlike the previous examples of nominals in action, her work is motivated primarily by proof-theoretical considerations: the ability to name leads to smoother proof systems.

#### Modal Proof Theory

And indeed, hybrid languages are proof-theoretically natural --
arguably more so than orthodox modal languages. Probably the most
straightforward way to see why, is to observe that the basic hybrid
language offers precisely what is needed to capture the main ideas of
labelled deduction. Labelled deduction, see [Gabbay 1996], is
built around the notation
. Here the meta-linguistic symbol : associates the meta-linguistic
label *l* with the object language formula
. This has a natural modal interpretation: regard labels as names for
states and read
as asserting that
is satisfied at *l*.
Labelled deduction proceeds by manipulating such labels to guide proof
search, and is today an important approach to modal proof theory.
The basic hybrid language places the apparatus of labelled deduction
in the *object* language: nominals are essentially object-level
labels, and the formula
asserts in the object
language what
asserts in the metalanguage. And
indeed, the basic hybrid languages turn out to be proof-theoretically
natural, for we can directly ``internalize'' standard labelled
deduction, see [Seligman 1997,Blackburn 1998]. Nonetheless, though
important,
is not indispensable. For example,
[Tzakova 1999] presents a general approa
ch to hybrid proof theory
using Fitting-style prefix calculi. And when the underlying modal
logic is temporal logic, even more flexibility is possible:
[Demri 1999] presents a sequent system for
nominal tense logic
*without*
that has much in common with the
-based internalized labelled deductive systems. Finally,
[Demri and Goré 1999] present a display calculi for nominal tense logic
with the difference operator
.