HyLo on Friday, August 11th
(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.
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.
||Valeria de Paiva
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.
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.
(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.
(LRI - Universite Paris Sud)
(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
(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.
(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
||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.
(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).
(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
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