M. Fitting. AddOns.

Abstract: The core of modal logic is elegantly simple: classical propositional logic with one extra operator, corresponding to a well-defined fragment of quantified classical logic. But over the years a number of addons have been proposed, all for good reasons. (As the film director Jean Renoir once said, ``The tragedy is, everyone has their reasons.'') In some ways these addons compromise the simplicity of the subject, but in other ways they enhance it. Adding machinery to refer to possible worlds is the addon most familiar to those attending this workshop. I will discuss two others, one propositional, one first-order. The propositional addon amounts to broadening the underlying logic from classical to many-valued. This provides us an alternative to standard formulations of logics of knowledge, and has ramifications that I am still exploring. When quantifiers are added to modal logic, a scoping mechanism similar to one introduced by Bertrand Russell becomes useful. This permits reasonable formal treatments of existence and denoting, makes possible a Herbrand theorem, and so on. How any of this relates to hybrid logic is anybody's guess, though. Clearly, what we are all engaged in is extending a familiar base, in the hopes of producing a natural extension. It is not the case that, once a subject is understood, things stop. .

C. Areces, P. Blackburn, M. Marx and U. Sattler. Welcome to the Workshop.

Abstract: To be provided.

C. Areces and C. Lutz. Concrete Domains and Nominals United.

Abstract: While the complexity of concept satisfiability in both ALCO, the basic description logic ALC enriched with nominals, and ALC(D), the extension of ALC with concrete domains, is known to be PSpace-complete, in this article we show that the combination ALCo(D) of these two logics can have a NExpTime-hard concept satisfiability problem (depending on the concrete domain D used). The proof is by a reduction of a NExpTime-complete variant of the domino problem to ALCO(D)-concept satisfiability.

T. Braüner. Natural Deduction for First-Order Hybrid Logic.

Abstract: This is a compainion to a previous paper where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relaitons and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem.

B. Heinemann. Axiomatizing Modal Theories of Subset Spaces (An Example of the Power of Hybrid Logic.

Abstract: This paper is about a synthesis of two quite different modal reasoning formalisms: the logic of subset spaces, and hybrid logic. Going beyond commonly considered languages we introduce names of objects involving sets and corresponding satisfaction operators. In thsi way we are able to completely axiomatize the theory of certain classes of subset spaces which are difficult to deal with purely modally. We also study effectivity properties of the resulting logical systems.

M. Vardi. Logic and Automata: Words, Trees, and Forests.

Abstract: One of the most fundamental results in mathematical logic is the Büchi-Elgot-Trakhtenbrot Theorem, established in the 1960s, which states that finite-state automata and monadic second-order logic (interpreted over finite words) have the same expressive power, and that the transformations from formulas to automata and vice versa are effective. In this talk, I survey the evolution of this beautiful connection and show how it provides an algorithmic tool set for automated reasoning for temporal logics, dynamic logics, and hybrid logics.

P. Blackburn and M. Marx. Constructive Interpolants for Every Bounded Fragment Definable Hybrid Logic.

Abstract: Craig's interpolation lemma (if A -> B is valid, then A -> C and C -> B are valid, for C a formula constructed using only primitive symbols which occur both in A and B) fails for many propositional modal logics. In first-order logic, there are even fewer examples of logics enjoying the property. The interpolation property is often regarded as a sign of well-matched syntax and semantics. The claim of hybrid logic is that modal logic is missing important syntactic machinery, namely tools for referring to worlds, and that adding such machinery solves many technical problems.
In the present paper we present strong evidence for this claim by defining interpolation algorithms for both propositional and first-order hybrid logic. These algorithms produce interpolants for the hybrid logic of every bounded fragment definable class of frames. In addition, on the class of all frames, the basic algorithm is conservative: on purely modal input it will compute interpolants in which the hybrid machinery does not occur.

P. Blackburn and B. ten Cate. Beyond Pure Axioms: Node Creating Rules in Hybrid Tableaux.

Abstract: We present a method of extending the tableau calculus for the basic hybrid language which automatically yields completeness results for many frame classes that cannot be defined by means of pure axioms (for example, Church-Rosser frames). The extended calculus makes use of node-creating rules. These rules trade on the idea of using nominals to perform skolemization on formulas of the strong hybrid language. Alternatively, viewing them from a Hilbert-style perspective, such rules can be viewed as a systematic generalization of Gabbay's irreflexivity rule. Our completeness result covers all frame classes definable by pure nominal-free universal existential sentences of the strong hybrid language. This properly includes all frame classes definable by universal existential first-order sentences.

R. de Freitas, J. Viana, P. Veloso, S. Veloso and M. Benevides. On Hybrid Arrow Logic.

Abstract: In this paper we investigate two approaches to hybridizing Arror Logic (AL). Hybridization is a general technique for increasing the power of modal logics: any modal logic my be `hybridized.' A hybrid extension of a given modal logic can be built in two stages. The first adds to the language a new sort of variables that will be formulas used to denote points in the domain of the frames. The second introduces mechanisms for handling additional information now available. There is a wide range of possibilities for the second step, the satisfiability operator and the down-arrow binder being the more intensively studied ones. The hybrid language H obtained from the basic modal language by introducing these two mechanisms, may be regarded as a kind of standard hybrid formalism. In this paper, we study a system obtained from a hybridization of AL, much as H was obtained from the basic modal language.

Adi Palm. Characterizing Tree-Adjoining Grammars with Hybrid Logic.

Abstract: Tree-Adjoining Grammars (TAG) are a tree rewriting system which captures mildly context sensitive phenomena in the syntax of some natural languages. However, the resulting sets of trees are not recognizable, i.e. there is no corresponding tree automaton accepting them. The same limitation applies to many logical formalisms on trees that consider at mist recognizable sets of trees. We present an approach based on hybrid logic that characterizes derived TAG trees and their corresponding derivation trees. By its modal foundation we obtain a simple formalism that provides - due to its hybrid elements - sufficient expressive power to specify axioms characterizing tree-adjoining grammars.

Hybrid Logics Site
Web Master: Carlos Areces

Copyright © 2002.