Hylo 2001. Third Workshop on Hybrid Logics
Third International Workshop on Hybrid Logic (HyLo 2001)
July 16th, 2001, Saarbrücken, Germany
HyLo 2001, the Third International Workshop on Hybrid Logic, was held at Computerlinguistik, Universität des Saarlandes, Saarbrücken, Germany, on 16th February 2001. The HyLo workshop series started in 1999 with a small closed workshop in Saarbrücken [3], followed by an open oneweek workshop during the ESSLLI 2000 summerschool in Birmingham, UK, which attracted an audience between 30 and 50 people a day. In these two years, hybrid logic started to take off as a subject on its own, getting input from a number of scientific fields. The third workshop brought together researchers from various disciplines with a common interest in hybrid languages. The 2001 autumn issue of the Journal of Logic and Computation will be a special issue on hybrid logic, based on presentations in the last two workshops. The fourth HyLo will be held in July 2002 as a satellite workshop to LICS in Denmark.
Before giving a short summary of the third HyLo workshop, 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 [5], the inventor of tense logic), were explored by Robert Bull [1], and were rediscovered and developed in new directions by the Sofia School in the 1980s (see, for example, [2,4]). 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.
HyLo 2001 was attended by researchers working in prooftheory, description logic, automated theorem proving, artificial intelligence and multi agent systems, and computational linguistics. After an overview of the current state of hybrid logic by Patrick Blackburn, five one hour talks were given. The abstracts of these talks are presented below, following the order of the workshop.
This workshop was made possible by a grant from the Dutch Science
Council NWO for cooperation between the Dutch Research School in
Logic OZSL and the
University of Saarbrücken.
The workshop was organized by Patrick Blackburn (INRIA/LORIA, Nancy,
France) and Maarten Marx (ILLC, University of
Amsterdam, The Netherlands).
Some prooftheoretic issues in Hybrid Logic
Jerry Seligman
Department of Philosophy, University of Auckland, New Zealand.
A sequent calculus for hybrid lgics is developed from a calculus for
classical predicate logic by a series of transformations. We formalize the
semantic theory of hybrid logic using a sequent calculus for predicate logic
plus axioms. This works, but it is ugly. The unattractive features are
removed onebyone, until the final vestiges of the metalanguage can be set
aside to reveal a fully internalized calculus. The techniques are quite
general and can be applied to a wide range of hybrid and modal logics.
Complexity of the Full Hybrid Calculus
or: the quest for the Queen of ExpTime Logics
Ulrike Sattler (joint work with Moshe Vardi)
RWTH Aachen, Aachen, Germany.
In the last years, several decision procedures for
ExpTimecomplete modal/description/ dynamic logics were implemented and
proved to behave well in practice. Due to its high expressive power,
the full Calculus (including converse programs) is one of the
``queens'' of ExpTime modal/description/dynamic logics. However, it
lacks two features important in many applications: nominals to refer
to named individuals, and a universal program for the internalisation
of general axioms. We present an ExpTime decision procedure for the
full Calculus extended with nominals and a universal program, thus
creating a new, more expressive ``queen'' logic. The decision
procedure is based on tree automata, and makes explicit the problems
caused by nominals and how to overcome them. Roughly speaking, we show
how to reason in a logic lacking the tree model property using
techniques for logics with the tree model property. Hence the
contribution of the paper is twofold: we extend the choice of ExpTime
logics an implementer can choose from, and we present a technique to
reason in the presence of nominals.
A Modal Logic for Network
Topologies
Wiebe van
der Hoek (joint work with Rogier van Eijk, Frank de Boer and
JohnJules Meyer)
Institute of Information and Computing Sciences, Utrecht University, The Netherlands.
We present a logical framework
that combines modality with a firstorder variablebinding mechanism.
The logic differs from standard firstorder modal logics in that
quantification is not performed inside the worlds of a model, but the
worlds in the model themselves constitute the domain of
quantification. The locality principle of modal logic is maintained
via the assumption that in each world the domain of quantification is
given by a subset of the entire set of worlds in the model. The
framework clearly separates the mechanisms of navigation and
variablebinding, and additionally allows one to reason about the
equalities and inequalities of the worlds of a model. Consequently, it
can be viewed upon as a basic framework to study for instance the
mechanisms and operations that have been developed in the area of
hybrid languages. We show that the logic is semantically
characterised by a generalisation of classical bisimulation, called
historybased bisimulation, address decidability issues and study the
application of the logic to describe and reason about network
topologies.
Fibring Labelled Deduction Systems
Luca Viganò
Institute für Informatik, AlbertLudwigsUniversität,
Freiburg,
Germany.
We give a categorial characterization of how labelled
deduction systems for logics with a propositional basis behave under
unconstrained fibring and under fibring that is constrained by
symbol sharing. At the semantic level, we introduce a general
semantics for our systems and then give a categorial
characterization of fibring of models. Based on this, we establish
the conditions under which our systems are sound and complete with
respect to the general semantics for the corresponding logics, and
establish requirements on logics and systems so that completeness is
preserved by both forms of fibring.
Inputoutput logics
Leon van der Torre
Department of Artificial Intelligence, Vrije Universiteit Amsterdam,
The Netherlands.
In a range of contexts, one comes across processes resembling inference,
but where input propositions are not in
general included among outputs, and the operation is not in any way
reversible. Examples arise in contexts of
conditional obligations, goals, ideals, preferences, actions, and
beliefs. Our purpose is to develop a general theory
of propositional input/output operations. Particular attention is given
to the special case where outputs may be
recycled as inputs.
Bibliography

 1

R. Bull.
An approach to tense logic.
Theoria, 36:282300, 1970.  2

G. Gargov and S. Passy (1988).
Determinism and Looping in Combinatory PDL.
Theoretical Computer Science, 61:259277.  3

M. Marx.
First International Workshop on Hybrid Logic (HyLo'99)
Logic Journal of the IGPL, 7:665669, 1999.  4

S. Passy and T. Tinchev.
An essay in combinatory dynamic logic.
Information and Computation, 93:263332, 1991.  5

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