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 ${\cal ALC}$, 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 $\atnom_{i}$ 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 $\atnom$ 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], $\downarrow$ 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 $l\!:\!\varphi$ . Here the meta-linguistic symbol : associates the meta-linguistic label l with the object language formula $\varphi$ . This has a natural modal interpretation: regard labels as names for states and read $l\!:\!\varphi$ as asserting that $\varphi$ 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 $\atnom_i\varphi$ asserts in the object language what $i\!:\!\varphi$ 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, $\atnom$ 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 $\atnom$ that has much in common with the $\atnom$ -based internalized labelled deductive systems. Finally, [Demri and Goré 1999] present a display calculi for nominal tense logic with the difference operator $\dmodop$.