Hylo'99. First Workshop on Hybrid Logics

First International Workshop on Hybrid Logic (HyLo'99)

July 13th, 1999, Saarbrücken, Germany

HyLo'99, the First International Workshop on Hybrid Logic, was held at Computerlinguistik, Universität des Saarlandes, Saarbrücken, Germany, on 13th July 1999. Organized to coincide with Jerry Seligman's visit to Europe, this closed workshop had two aims: to bring together researchers in hybrid languages to present recent developments, and to discuss how best to stimulate interest in the subject.

Before going further, a little background may be helpful. The simplest example of a hybrid language is a modal language enriched with special propositional symbols (nominals) that name states. More generally, hybrid languages are modal languages whose propositional symbols are sorted, the interpretation of each sort being constrained appropriately (nominals, for example, have to be true at exactly one state in any model). More expressive hybrid languages may permit certain sorts of atoms to be bound in various ways.

Hybrid languages date back to at least the late 1960s (they are due to Arthur Prior [10], the inventor of tense logic), were explored by Robert Bull [4], and were rediscovered and developed in new directions by the Sofia School in the 1980s (see, for example, [7,9]). In the last few years there has been a resurgence of interest, with new results in expressivity, interpolation, complexity, and proof theory. Moreover, it has also become clear that hybrid logics offer a theoretical framework for integrating the work of a surprisingly diverse range of research traditions, such as description logic, rough set theory and logics of similarity, labelled deduction, and feature logic. A number of recent publications are listed below.

HyLo`99 was the first workshop solely devoted to hybrid logic. The morning session examined general issues in hybrid logic and their relation to other frameworks. Three talks were given, and all adopted a largely model-theoretic perspective:

Hybrid Languages
Patrick Blackburn
Computerlinguistik, Universität des Saarlandes, Saarbrücken, Germany.
Patrick gave an overview of hybrid languages that introduced various key concepts such as nominals, the @ operator, the various hybrid binders now commonly used (notably \downarrow and \exists), and other tools (such as the universal modality, and the difference operator D) encountered in the literature on hybrid languages. As well as outlining the `mainstream' history of hybrid languages, Patrick drew attention to many other formalisms which can be viewed as variants or subsystems.

Hybrid Logic and Description Logic
Carlos Areces
ILLC, University of Amsterdam, The Netherlands.
While the basic link between hybrid languages and description logic has long been clear (the one-of operator \cal{O} corresponds to disjunctions of nominals, and A-box reasoning corresponds to restricted use of @), Carlos's talk made the link tighter and more interesting. After giving a clear introduction to description languages, he gave a neat account of which hybrid fragments correspond to certain key description languages. Second, he showed how a (polynomial space decidable) fragment of the hybrid language with @ and \downarrow could be used to define concepts beyond the reach of standard description logics: his examples (self-employed and lucky-lover) were clear and convincing.

Locality
Maarten Marx
Department of Artificial Intelligence, Free University, Amsterdam, The Netherlands.
The hybrid language in @ and \downarrow picks out precisely the bounded fragment of first order logic (that is, the first-order formulas invariant under generated submodels; see [1]). Thus @ and \downarrow capture an important aspect of locality, a key property of modal logics. On the other hand, various guarded fragments are clearly modal too (they arise by generalizing the Standard Translation of modal logic into first-order logic). But the guarded and bounded fragments are very different (among other things, the former is decidable, while the latter is not). How can two such different fragments both claim to be genuinely modal? Maarten's talk resolved the tension by introducing finer grained versions of locality based on the notion of a packed set . This lead to an interesting discussion of the potential relevance of this issue to description logics, and the possibility of hybrid languages with sorts ranging over cliques.

Following this we adjourned for lunch - and returned to an afternoon session devoted to proof theory. Proof theory for hybrid languages was pioneered by Jerry Seligman in the early 1990s (at present [11] is the only widely available source for his work). In independent work in the mid 1990s, nominals were added to similarity logics to improve their proof-theoretical properties (see Konikowska [8]). More recently there have been a number of papers devoted to non-Hilbert style proof systems for various hybrid languages (see, for example, Blackburn [3] and Tzakova [12]). Moreover, it has become clear that there are important links between hybrid deduction and work in the Labelled Deductive System tradition. With four talk devoted to such topics, we were surely in for an interesting session:

Cut-Free Display Calculi for Nominal Tense Logics
Rajeev Goré
Automated Reasoning Project and Department of Computer Science, Australian National University, Canberra, Australia.
Rajeev's talk, based on [6], his recent joint Tableaux'99 paper with Stéphane Demri, introduced a new style of proof system for hybrid languages: display calculi. (Most previous non-axiomatic proof systems for hybrid languages have been tableau, sequent, or natural-deduction based.) After introducing display calculi, Rajeev turned to the question of displaying nominals. The key idea was to use the difference operator to extend Wansing's strong normalization theorem; the approach was clearly motivated and well-explained. After the talk the following question was raised and discussed: is it possible to obtain well behaved display calculi based on the weaker @ operator, rather than the difference operator?

Labelled Non-Classical Logics
Luca Viganò
Institute für Informatik, Albert-Ludwigs-Universität, Freiburg, Germany.
Broadly speaking, Luca's talk (based on joint work with David Basin and Seán Matthews [2]) belongs to the labelled deductive system tradition - but one of the key points Luca made was that labelling and labelled deduction comes in many varieties, and general results in labelled deduction need not trade on (implicit or explicit) use of the Standard Translation. To demonstrate this, Luca discussed a number of different ways of handling \bot in labelled deduction, noting various proof theoretical tradeoffs. He concluded by discussing recent work on proof theoretical analyses of modal complexity. His talk, and the subsequent discussion, made clear there are links between hybrid languages and labelled deduction that deserve further exploration. It was also interesting to observe how close the tools he was using were to the fragments of hybrid languages isolated by Carlos in his talk on description logics.

Internalization
Jerry Seligman
Department of Philosophy, University of Auckland, New Zealand.
The internal approach to hybrid deduction trades on the insight that @ and nominals can be viewed as reflecting the modal satisfaction definition. In his talk, Jerry began with an external approach to modal reasoning, based on a fully formalized first-order metalanguage, and step-by-step showed how to develop internalized calculi. A number of interesting points emerged. For a start, something close to the labelling methods discussed by Luca seemed to be a natural intermediate stage in this process. Second, Jerry emphasized that his approach offered a number of results (notably concerning completeness and interpolation) for free: the first-order metalanguage has these properties, and his internalization process is carried out in ways that either prevents a property being lost (completeness) or allows it to be recovered (interpolation).

Sequent Calculi for Nominal Tense Logics
Stéphane Demri
Laboratoire LEIBNIZ - C.N.R.S., Grenoble, France.
Stéphane's talk was based on his recent Tableaux'99 paper [5], which defines a sequent calculus for nominal tense logic. Roughly speaking, his calculus is an internalized one (it doesn't use metalinguistic prefixes or labels but relies solely on the resources available in the object language), but he achieves this internalization without the help of the @ operator. Also interesting was Stéphane's account of how this calculus arose: in essence he used the difference operator to help design the system, but avoided having to introduce D into the object language. Stéphane also posed a methodological challenge. In contrast to most of the other participants, he felt that many of the proof methods discussed were not, in the end, so very different from classical first-order methods - a view which lead to spirited discussion.

All in all, HyLo`99 was a highly successful workshop. The standard of both talks and discussion was high, and there was genuine exchange of ideas. Indeed, its only real shortcoming was that the range of participants was too narrow: it would have been highly desirable to have representatives of the description logic and similarity logic communities, for example. In the business meeting that followed the talks, it was decided to organize an open workshop in the year 2000, a workshop explicitly devoted to attracting as wide a range of participants as possible. It was abundantly clear to all participants that the time is now ripe to draw together the many threads that make up hybrid logic.

Pictures from the Event

References

[1]

C. Areces, P. Blackburn, and M. Marx (1999). Hybrid logics. Characterization, interpolation and complexity. CLAUS-Report 104, Computerlinguistik, University of Saarland, .

[2]

D. Basin, S. Matthews, L. Viganò (1997). Labelled propositional modal logics: Theory and practice. Journal of Logic and Computation, 7:685-717.

[3]

P. Blackburn (1998). Internalizing labelled deduction. Technical Report CLAUS-Report 102, Computerlinguistik, Universität des Saarlandes. .

[4]

R. Bull (1970). An approach to tense logic. Theoria, 36:282-300.

[5]

S. Demri (1999). Sequent calculi for nominal tense logics: a step towards mechanization? In N. Murray (ed.), Conference on Tableaux Calculi and Related Methods (TABLEAUX), Saratoga Springs, USA, pages 140-154, Springer Verlag, LNAI 1617.

[6]

S. Demri and R. Goré (1999). Cut-free display calculi for nominal tense logics. In N. Murray (ed.), Conference on Tableaux Calculi and Related Methods (TABLEAUX), Saratoga Springs, USA, pages 155-170, Springer Verlag, LNAI 1617.

[7]

G. Gargov and S. Passy (1988). Determinism and looping in combinatory PDL. Theoretical Computer Science, 61:259-277.

[8]

B. Konikowska (1997). A logic for reasoning about relative similarity. Studia Logica, 58:185-226.

[9]

S. Passy and T. Tinchev (1991). An essay in combinatory dynamic logic. Information and Computation, 93:263-332.

[10]

A. Prior (1967). Past, Present and Future. Oxford University Press, Oxford.

[11]

J. Seligman (1997). The logic of correct description. In M. de Rijke (ed.), Advances in Intensional Logic, pages 107-135. Applied Logic Series, Kluwer.

[12]

M. Tzakova (1999). Tableaux calculi for hybrid logics. In N. Murray (ed.), Conference on Tableaux Calculi and Related Methods (TABLEAUX), Saratoga Springs, USA, pages 278-292, Springer Verlag, LNAI 1617.