HyLo on Saturday, July 10th

09:00‑09:50 Session 1
Location: AT 2.11
09:00 Dario Della Monica, Valentin Goranko and Guido Sciavicco
Hybrid Metric Propositional Neighborhood Logics with Interval Length Binders

We investigate the question of how much hybrid machinery can be added to the interval neighbourhood logic PNL and its metric extension MPNL without losing the decidability of their satisfiability problem in $\Nat$. In particular, we consider the natural hybrid extension of MPNL obtained by adding binders on integer variables ranging over lengths of intervals, thus enabling storage of the length of the current interval and further references to it. We show that even the weakest natural fragment of such extensions becomes undecidable, which is somewhat surprising, being in sharp contrast with the decidability of MPNL, which can be seen as a hybrid language with length constraints only involving constants over interval lengths. These results show that MPNL itself is, in this sense, a maximal decidable (weakly) hybrid extension of PNL.

09:30 Michael R. Hansen
Efficient Model Checking for a Hybrid Duration Calculus

Recently in \cite{FraenzleHansenSEFM08,FH09}, a model checking result has been developed for a rich subset of DC. This result is based on branching-time approximations and a first prototype implementation has illustrated that the approximations seem fine grained enough to give useful results. The aim of this work-in-progress is to extend this model-checking technique to a hybrid version of Duration Calculus.

10:30‑12:30 Session 2
Location: AT 2.11
10:30 Moshe Vardi (Rice University)
Hybrid Logic: The Search for The Decidability Frontier

The past decade has seen an intensive research program in expressive hybrid logics, trying to chart the frontiers separating the decidable from the undecidable and the tractable from the intractable. This quest was accompanied by the development of powerful automata-theoretic machinery, which underlies all decidability results. This talk surveys both developments.

11:30 Arne Meier, Martin Mundhenk, Thomas Schneider, Michael Thomas and Felix Weiss
The Complexity of Satisfiability for Fragments of Hybrid Logic --- Part II

Hybrid logic is an expressive specification language, but has an undecidable satisfiability problem in general. In this paper, we restrict the set of Boolean operators to monotone operators (for instance conjunction and disjunction) and the underlying frames to commonly used acyclic frames, namely transitive trees, total transitive trees, linear orders, and the natural numbers. We show that, under these restrictions, satisfiability is decidable for 16 fragments arising from different combinations of modal and hybrid operators. More precisely, we categorise these fragments to be PSPACE-complete, NP-complete or tractable, where the latter cases are contained in detLOGCFL or complete for $NC1$.

12:00 Jens Ulrik Hansen
A Hybrid Public Announcement Logic with Distributed Knowledge

In this paper the machinery of hybrid logic and the logic of public announcements are merged. In order to bring the two logics together, one must make a choice: to change the hybrid logic such that nominals only partially denote states. Changing the hybrid logic this way will be discussed in detail. Following this, an axiom system for the hybrid public announcement logic is presented and using reduction axioms general completeness (in the style of hybrid logic) is proved. In addition, distributive knowledge is added. By generalizing this approach, other modalities may be added.

14:00‑15:00 Session 3
Location: AT 2.11
14:00 Gert Smolka (Saarland University)
Tableau-Based Decision Procedures for Hybrid Logic

The talk will review ongoing work with Mark Kaminski on terminating tableaux for hybrid logic with difference and star modalities. Of particular interest are the representation of nominal equality and the structure that provides for termination. I will first review prefixed approaches with chain-based and pattern-based blocking. Then I will discuss our new prefix-free approach that employs clausal tableaux.

15:30‑16:50 Session 4
Location: AT 2.11
15:30 Valeria de Paiva, Hermann Hausler and Alexandre Rademaker
Constructive Description Logic, Hybrid-Style

Description logics are very popular right now. Given the existent and proposed applications of the Semantic Web, there has been a fair amount of work into finding the most well-behaved system of description logic that has the broadest application. As discussed in \cite{depaiva2003}, considering versions of {\em constructive} description logics makes sense, both from a theoretical and from a practical viewpoint. There are several possible and sensible ways of defining {\em constructive} description logics, as explained in \cite{depaiva2003}. In particular Mendler and Scheele have worked out a very compelling system (\cite{mendler-scheele}), but in this note we follow a different path and describe a constructive version of \alc, based on the framework for constructive modal logics developed by Simpson in his phd thesis \cite{simpson95}.

Our motivation is the constructive framework developed by Brauner and de Paiva in \cite{brauner-depaiva2006} for Hybrid Logics. We reason that having already frameworks for constructive modal and constructive hybrid logics in the labelled style of Simpson, we might end up with the best style of constructive description logics, in terms of both worked out foundations and ease of implementation.

We first recall Simpson's framework for constructive modal logics and Brauner and de Paiva's systems for constructive hybrid logics. Then to introduce our version of intuitionistic description logic, denoted $\ialc$, we proceed in three steps. First we describe a simplified form of Mendler and Scheele's system that, unlike their system, satisfies distribution of existentials over nullary disjunction $\bot$. Then we modify the system to a labelled one, where labels are worlds as in Simpson's work. Finally we change the approach to deal with labels as in Rademaker and Hausler's previous work.

15:50 Søren Lind Kristiansen and Anders Søgaard
Querying dependency treebanks using hybrid logic

Existing logic-based querying tools for dependency treebanks use first order logic or monadic second order logic. We introduce a very fast model checker based on hybrid logic with operators ↓, @ and A and show that it is much faster than existing querying tools as well as a general purpose hybrid logic model checker. The querying tool is made publicly available.

16:10 Katsuhiko Sano
Axiomatizing Hybrid Products of Monotonic Neighborhood Frames

The main aim of this paper is to propose a robust way to combine two monotonic hybrid logics. This work can be regarded as a further extension of both topological semantics for hybrid logic (Ten Cate and Litak 2007) and bi-hybrid logic of products of Kripke frames (Sano, forthcoming). First, we generalize the notion of product of topologies (Van Benthem, et al 2006) to the monotonic neighborhood frames and introduce two kinds of: nominals: $i$ (e.g. for a moment of time) and $a$ (e.g. for a spatial point), and satisfaction operators: $@_{i}$ and $@_{a}$ to describe a product of monotonic neighborhood frames. Second, we give five interaction axioms and establish a general completeness result called pure completeness of bi-hybrid logic of monotonic neighborhood frames. By extending this, we also establish a pure completeness result of bi-hybrid logic of products of topologies.

16:30 Thomas Bolander
Two approaches to termination and completeness for hybrid tableaus

This paper studies two different approaches to termination and completeness for hybrid tableau calculi, here called the "direct" and "reduction" method, respectively. The direct method is by far the most widespread and well understood in connection with tableau calculi for hybrid and description logics. The reduction method has not previously been employed in connection with hybrid tableaus. The article presents both methods, and compare their respective advantages and disadvantages. In particular, we provide general results concerning the termination and completeness of tableau calculi for hybrid logics on various frame classes using both methods.