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 one-week 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 proof-theory, 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 proof-theoretic 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 one-by-one, 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 ExpTime-complete 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 two-fold: 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 John-Jules Meyer)
Institute of Information and Computing Sciences, Utrecht University, The Netherlands.
We present a logical framework that combines modality with a first-order variable-binding mechanism. The logic differs from standard first-order 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 variable-binding, 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 history-based 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, Albert-Ludwigs-Universitä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.

Input-output 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.