HyLo on Friday, August 11th

Opening (08:55‑09:00)

Session 1 (09:00‑10:30)

09:00‑10:00

Patrick Blackburn (INRIA Lorraine, France) Hybrid Logic and Temporal Semantics Hybrid logic is historically linked with temporal semantics for natural language; in fact, Arther Prior originally developed hybrid logic in order to have a modal logic of time strong enough to model the temporal expressivity of natural language. But while technical results have been obtained for various types of hybrid temporal logic (notably point-based and interval-based systems) there has been relatively little work on developing the connection with natural language; even Prior himself wrote little on the topic. The time seems ripe to start exploring this connection again. For a start, the development of temporal markup languages (such as TimeML) has lead to an explosion of interest within computational linguistics in coping reliably with temporal information. Hybrid logic seems to fit in naturally with such formalisms, and could be used to interpret them. And relatively simple adaptations make it possible for hybrid logics to cope with a wide range of temporal phenomena. But to make hybrid logic useful in this area we have to move beyond the setting of propositional hybrid logic (where most research has concentrated) to first-order and even higher-order temporal logics. In this talk I will discuss the sort of problems that need to be modelled, the sort of expressivity needed to cope with natural language applications, and will present hybrid languages suitable for this purpose (probably including a Montague-style Hybrid Intensional Logic). Time permitting, I will also discuss the links with TimeML.

10:00‑10:30

Moritz Hardt (Saarland University) Gert Smolka (Saarland University) Higher-Order Syntax and Saturation Algorithms for Hybrid Logic We present modal logic on the basis of the simply typed lambda calculus with a system of equational deduction. Combining first-order quantification and higher-order syntax, we can maintain modal reasoning in terms of classical logic by remarkably simple means. Such an approach has been broadly uninvestigated, even though it has notable advantages, especially in the case of Hybrid Logic. We give an alternative characterization of HL(@) and develop a tableau-based decision procedure for this logic. Our algorithm guarantees termination by local criteria, which is in contrast to previous decision procedures. With regards to deduction, we simplify in particular the treatment of identities. Traditionally, modal tableau calculi either rely on external labeling mechanisms or have to represent an accessibility relation by equivalent formulas. In our system labeling and access information are both internal and explicit. With regards to space consumption, we provide an optimal formulation of our saturation algorithm. This proves the satisfiability problem for HL(@) to be in PSPACE, a result that was previously not achieved by the saturation approach.

Break (10:30‑11:00)

Session 2 (11:00‑12:30)

11:00‑12:00

Valeria de Paiva (PARC, USA) Constructive Hybrid Logics and Contexts [pdf] One of the (several) origins of hybrid logics was the early work of Seligman on a logic of correct descriptions. This work was also one of the basis for the work (by Torben Braüner and myself) on a Natural Deduction formulation of constructive hybrid logic. The system described by Seligman seems intuitive and appealing as a logic of contexts for AI, but this intuition has not been made very precise, yet. Giving an invited talk is the perfect excuse to try to ascertain the pros and cons of a logic of contexts based on constructive hybrid logics, as opposed to one based on constructive modal logics.

12:00‑12:30

Martin Mundhenk (Friedrich-Schiller-Universitaet Jena) Thomas Schneider (Friedrich-Schiller-Universitaet Jena) Undecidability of Multi-modal Hybrid Logics This paper establishes undecidability of satisfiability for multi-modal logic equipped with the hybrid downarrow-binder, with respect to frame classes over which the same language with only one modality is decidable. This is in contrast to the usual behaviour of many modal and hybrid logics, whose uni-modal and multi-modal versions do not differ in terms of decidability and, quite often, complexity. The results from this paper apply to a wide range of frame classes including temporally and epistemically relevant ones.

Lunch break (12:30‑14:00)

Session 3 (14:00‑15:30)

14:00‑15:00

Ian Horrocks (University of Manchester, UK) Hybrid Logics and Ontology Languages [ppt] Description Logics (DLs) are a family of logic based knowledge representation formalisms. Although they have a range of applications, they are perhaps best known as the basis for widely used ontology languages such as OIL, DAML+OIL and OWL, the last of which is now a World Wide Web Consortium (W3C) recommendation. SHOIQ, the DL underlying OWL DL (the most widely used "species" of OWL), includes familiar features from hybrid logic. In particular, in order to support extensionally defined classes, SHOIQ includes nominals: classes whose extension is a singleton set. This is an important feature for a logic that is designed for use in ontology language applications, because extensionally defined classes are very common in ontologies. Binders and state variables are another feature from Hybrid Logic that would clearly be useful in an ontology language, but it is well known that adding this feature to even a relatively weak language would lead to undecidability. However, recent work has shown that this feature could play a very useful role in query answering, where the syntactic structure of queries means that the occurrence of state variables is restricted in way that allows for decidable reasoning.

15:00‑15:30

Nicole Bidoit (LRI - Universite Paris Sud) Dario Colazzo (LRI - Universite Paris Sud) Testing XML constraint satisfiability In a previous paper, we have showed that Hybrid Modal Logic can be successfully used to modelize semistructured data and provides a simple and well suited formalism for capturing ``well typed'' references and of course a powerfull language for expressing constraint. This paper builds on the previous one and provides a tableau proof technique for constraint satisfiability testing in the presence of schemas.

Break (15:30‑16:00)

Session 4 (16:00‑18:30)

16:00‑16:30	Andre Platzer (Carnegie Mellon University) Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems We introduce a hybrid variant of a dynamic logic with continuous state transitions along differential equations, and we present a sequent calculus for this extended hybrid dynamic logic. With the addition of satisfaction operators, this hybrid logic provides improved system introspection by referring to properties of states during system evolution. In addition to this, our calculus introduces state-based reasoning as a paradigm for delaying expansion of transitions using nominals as symbolic state labels. With these extensions, our hybrid dynamic logic advances the capabilities for compositional reasoning about (semi-algebraic) hybrid dynamic systems. Moreover, the constructive reasoning support for goal-oriented analytic verification of hybrid dynamic systems carries over from the base calculus to our extended calculus.
16:30‑17:00	Tadeusz Litak (School of Information Science, JAIST) Balder ten Cate (ISLA - Informatics Institute, University of Amsterdam) Topological Perspective on the Hybrid Proof Rules We consider the non-orthodox proof rules of hybrid logic from the viewpoint of topological semantics. Topological semantics is more general than Kripke semantics. We show that the hybrid proof rule [BG] is topologically not sound. Indeed, among all topological spaces the [BG] rule characterizes those that can be represented as a Kripke frame (i.e., the Alexandroff spaces). We also demonstrate that, when the [BG] rule is dropped and only the [Name] rule is kept, one can prove a general topological completeness result for hybrid logics axiomatized by pure formulas. Finally, we indicate some limitations of the topological expressive power of pure formulas. All results generalize to neighborhood frames.
17:00‑17:30	Katsuhiko Sano (Graduate School of Letters, Kyoto University) A Hybridization of Irreflexive Modal Logics This paper discusses a bimodal hybrid language with a sub-modality (called the irreflexive modality) associated with the intersection of the accessibility relation R and the inequality. First, we provide the Hilbert-style axiomatizations (with and without the COV-rule) for logics of our language, and prove the Kripke completeness and the finite frame property for them. Second, with respect to the frame expressive power, we compare our language containing the irreflexive modality with the unimodal hybrid language H. Finally, we establish the Goldblatt-Thomason-style characterization for our language.
17:30‑18:00	Thomas Bolander (Technical University of Denmark) Jens Ulrik Hansen (University of Copenhagen) Michael Reichhardt Hansen (Technical University of Denmark) Decidability of a Hybrid Duration Calculus We present a hybrid logical version of Restricted Duration Calculus (RDC), and show that this logic is decidable by reducing the satisfiability problem to satisfiability of Weak Second-Order Monadic Logic of one successor (WS1S).
18:00‑18:30	Jason Reed (Carnegie Mellon University) Hybridizing a Logical Framework Logical connectives familiar from the study of hybrid logic can be added to the logical framework LF, a constructive type theory of dependent functions. This extension turns out to be an attractively simple one, and maintains all the usual theoretical and algorithmic properties, for example decidability of type-checking. Moreover it results in a rich metalanguage for encoding and reasoning about a range of resource-sensitive substructural logics, analagous to the use of LF as a metalanguage for more ordinary logics. This family of applications of the language, contrary perhaps to expectations of how hybridized systems are typically used, does not require the usual modal connectives box and diamond, nor any internalization of a Kripke accessibility relation. It does, however, make essential use of distinctively hybrid connectives: universal quantifiation over worlds, truth of a proposition at a named world, and local binding of the current world. This supports the claim that the innovations of hybrid logic have independent value even apart from their traditional relationship to temporal and alethic modal logics.