
Abstracts 
M. Fitting. AddOns. 
Abstract: The core of modal logic is elegantly simple: classical propositional logic with one extra operator, corresponding to a welldefined 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 firstorder. The propositional addon amounts to broadening the underlying logic from classical to manyvalued. 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 PSpacecomplete, in this article we show that the combination ALCo(D) of these two logics can have a NExpTimehard concept satisfiability problem (depending on the concrete domain D used). The proof is by a reduction of a NExpTimecomplete variant of the domino problem to ALCO(D)concept satisfiability.

[PostscriptPDF] 
T. Braüner. Natural Deduction for FirstOrder 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 firstorder case. Our natural deduction system for firstorder hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relaitons and the quantifier domains expressed by socalled geometric theories. We prove soundness and completeness and we prove a normalisation theorem.

[PostscriptPDF] 
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.

[PostscriptPDF] 
M. Vardi. Logic and Automata: Words, Trees, and Forests. 
Abstract: One of the most fundamental results in mathematical logic is the BüchiElgotTrakhtenbrot Theorem, established in the 1960s, which states that finitestate automata and monadic secondorder 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 firstorder logic, there are even fewer
examples of logics enjoying the property. The interpolation
property is often regarded as a sign of wellmatched 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.

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, ChurchRosser frames). The extended calculus makes use of nodecreating 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 Hilbertstyle 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 nominalfree universal existential sentences of the strong hybrid language. This properly includes all frame classes definable by universal existential firstorder sentences.

[PostscriptPDF] 
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 downarrow 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.

[PostscriptPDF] 
Adi Palm. Characterizing TreeAdjoining Grammars with Hybrid Logic. 
Abstract: TreeAdjoining 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 treeadjoining grammars.

Hybrid Logics Site Web Master: Carlos Areces Copyright © 2002. 