
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
The Workshop |
![]() |
![]() |
![]() |
The Workshop's Breakfast |
![]() |
![]() |
![]() |
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.