In their simplest form, hybrid languages are propositional modal languages which can refer to states. They were introduced by Arthur Prior, the inventor of tense logic, and played an important role in his work: because they make reference to specific times possible, they remove the most serious obstacle to developing modal approaches to temporal representation and reasoning. However very little is known about the computational complexity of hybrid temporal logics.In this paper we analyze the complexity of the satisfiability problem of (...) a number of hybrid temporal logics: the basic hybrid language over transitive trees; nominal Until logic; and referential interval logic. We discuss the effects of including nominals, the @ operator, the somewhere modality E, and the difference operator D. Adding nominals to tense logic leads for several frame-classes to an increase in complexity of the satisfiability problem from PSPACE to EXPTIME. On transitive trees, however, the satisfiability problem for this language can be decided in PSPACE. Along the way we make a detour through hybrid propositional dynamic logic: we establish upper bounds for a number of temporal logics by generalizing results due to Passy and Tinchev [29] and De Giacomo [16]. We conclude with some remarks on the relevance of our results to description logic, and draw attention to the utility of the spypoint technique for proving upper and lower bounds. (shrink)

Spatial reasoning is essential for many AI applications. In most existing systems the representation is primarily numerical, so the information that can be handled is limited to precise quantitative data. However, for many purposes the ability to manipulate high-level qualitative spatial information in a flexible way would be extremely useful. Such capabilities can be proveded by logical calculi; and indeed 1st-order theories of certain spatial relations have been given [20]. But computing inferences in 1st-order logic is generally intractable unless special (...) methods are known.0-order modal logics provide an alternative representation which is more expressive than classical 0-order logic and yet often more amenable to automated deduction than 1st-order formalisms. These calculi are usually interpreted as propositional logics: non-logical constants are taken as denoting propositions. However, they can also be given a nominal interpretation in which the constants stand for some kind of object. I show how 0-order logics can be given a spatial interpretation: constants denote regions and logical operators correspond to operations on regions which are important for characterising spatial situations.Representing certain spatial concepts requires the introduction of modal operators, interpreted as functions generating regions related in specific ways to those denoted by their arguments. A significant example is the convex-hull operator whose value is the smallest convex region containing its argument. I investigate how this this operator can be captured in a multi-medal logic. (shrink)

ABSTRACT The paper studies propositional logics in a bimodal language, in which the first modality is interpreted as the local truth, and the second as the universal truth. The logic S4UC is introduced, which is finitely axiomatizable, has the f.m.p. and is determined by every connected separable metric space.