Citations of:
Modal logic with names
Journal of Philosophical Logic 22 (6):607  636 (1993)
Add citations
You must login to add citations.


Hybrid languages are expansions of propositional modal languages which can refer to (or even quantify over) worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work (for example [BS98, BT98a, BT99]) has focussed on a more constrained system called $\mathscr{H}(\downarrow, @)$ . We show in detail that $\mathscr{H}(\downarrow, @)$ is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations (via a restricted notion of EhrenfeuchtFraisse game, and an enriched notion of (...) 

In this paper we argue that hybrid logic is the deductive setting most natural for Kripke semantics. We do so by investigating hybrid axiomatics for a variety of systems, ranging from the basic hybrid language to the strong Priorean language . We show that hybrid logic offers a genuinely firstorder perspective on Kripke semantics: it is possible to define base logics which extend automatically to a wide variety of frame classes and to prove completeness using the Henkin method. In the (...) 

In this paper we study the expressive power and definability for modal languages interpreted on topological spaces. We provide topological analogues of the van Benthem characterization theorem and the Goldblatt–Thomason definability theorem in terms of the wellestablished firstorder topological language. 

A complete axiomatic system CTL$_{rp}$ is introduced for a temporal logic for finitely branching $\omega^+$trees in a temporal language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL$^{*}$ into CTL$_{rp}$. In particular, that yields a complete axiomatization for the translations of all valid CTL$^{*}$formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a way more expressive medium for reasoning (...) 



In this paper we argue that Prior and Reichenbach are best viewed as allies, not antagonists. We do so by combining the central insights of Prior and Reichenbach in the framework of hybrid tense logic. This overcomes a wellknown defect of Reichenbach’s tense schema, namely that it gives multiple representations to sentences in the future perfect and the futureinthepast. It also makes it easy to define an iterative schema for tense that allows for multiple points of reference, a possibility noted (...) 

In [14], we studied the computational behaviour of various firstorder and modal languages interpreted in metric or weaker distance spaces. [13] gave an axiomatisation of an expressive and decidable metric logic. The main result of this paper is in showing that the technique of representing metric spaces by means of Kripke frames can be extended to cover the modal (hybrid) language that is expressively complete over metric spaces for the (undecidable) twovariable fragment of firstorder logic with binary predicates interpreting the (...) 

Hybrid languages have both modal and firstorder characteristics: a Kripke semantics, and explicit variable binding apparatus. This paper motivates the development of hybrid languages, sketches their history, and examines the expressive power of three hybrid binders. We show that all three binders give rise to languages strictly weaker than the corresponding firstorder language, that full firstorder expressivity can be gained by adding the universal modality, and that all three binders can force the existence of infinite models and have undecidable satisfiability (...) 

We study term modal logics, where modalities can be indexed by variables that can be quantified over. We suggest that these logics are appropriate for reasoning about systems of unboundedly many reasoners and define a notion of bisimulation which preserves propositional fragment of term modal logics. Also we show that the propositional fragment is already undecidable but that its monodic fragment is decidable, and expressive enough to include interesting assertions. 

We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkinstyle completeness proofs even when the modal logic being hybridized is higherorder. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret $@_i$ in propositional and firstorder hybrid logic. This means: interpret $@_i\alpha _a$ , where $\alpha _a$ is an expression of any type $a$ , as an expression of type $a$ that (...) 

This paper contributes to the principled construction of tableaubased decision procedures for hybrid logic with global, difference, and converse modalities. We also consider reflexive and transitive relations. For conversefree formulas we present a terminating control that does not rely on the usual chainbased blocking scheme. Our tableau systems are based on a new model existence theorem. 



Many of the formalisms used in Attribute Value grammar are notational variants of languages of propositional modal logic, and testing whether two Attribute Value Structures unify amounts to testing for modal satisfiability. In this paper we put this observation to work. We study the complexity of the satisfiability problem for nine modal languages which mirror different aspects of AVS description formalisms, including the ability to express reentrancy, the ability to express generalisations, and the ability to express recursive constraints. Two main (...) 

We generalize and extend the class of Sahlqvist formulae in arbitrary polyadic modal languages, to the class of so called inductive formulae. To introduce them we use a representation of modal polyadic languages in a combinatorial style and thus, in particular, develop what we believe to be a better syntactic approach to elementary canonical formulae altogether. By generalizing the method of minimal valuations à la Sahlqvist–van Benthem and the topological approach of Sambin and Vaccaro we prove that all inductive formulae (...) 



We study hybrid logics in topological semantics. We prove that hybrid logics of separation axioms are complete with respect to certain classes of finite topological models. This characterisation allows us to obtain several further results. We prove that aforementioned logics are decidable and PSPACEcomplete, the logics of T 1 and T 2 coincide, the logic of T 1 is complete with respect to two concrete structures: the Cantor space and the rational numbers. 

The paper introduces a firstorder theory in the language of predicate tense logic which contains a single simple axiom. It is shewn that this theory enables times to be referred to and sentences involving ‘now’ and ‘then’ to be formalised. The paper then compares this way of increasing the expressive capacity of predicate tense logic with other mechanisms, and indicates how to generalise the results to other modal and tense systems. 

We survey main developments, results, and open problems on interval temporal logics and duration calculi. We present various formal systems studied in the literature and discuss their distinctive features, emphasizing on expressiveness, axiomatic systems, and (un)decidability results. 

On the 4th of December 1967, Hans Kamp sent his UCLA seminar notes on the logic of ‘now’ to Arthur N. Prior. Kamp’s twodimensional analysis stimulated Prior to an intense burst of creativity in which he sought to integrate Kamp’s work into tense logic using a onedimensional approach. Prior’s search led him through the work of Castañeda, and back to his own work on hybrid logic: the first made temporal reference philosophically respectable, the second made it technically feasible in a (...) 

Topic of the paper is Qlogic  a logic of agency in its temporal and modal context. Qlogic may be considered as a basal logic of agency since the most important stitoperators discussed in the literature can be defined or axiomatized easily within its semantical and syntactical framework. Its basic agent dependent operator, the Qoperator (also known as Δ or cstitoperator), which has been discussed independently by E v. Kutschera and B. E Chellas, is investigated here in respect of its (...) 



In this paper I present a dynamicepistemic hybrid logic for reasoning about information and intention changes in situations of strategic interaction. I provide a complete axiomatization for this logic, and then use it to study intentionsbased transformations of decision problems. 

In recent years combinations of tense and modality have moved intothe focus of logical research. From a philosophical point of view, logical systems combining tense and modality are of interest because these logics have a wide field of application in original philosophical issues, for example in the theory of causation, of action, etc. But until now only methods yielding completeness results for propositional languages have been developed. In view of philosophical applications, analogous results with respect to languages of predicate logic (...) 

Several extensions of the basic modal language are characterized in terms of interpolation. Our main results are of the following form: Language ℒ' is the least expressive extension of ℒ with interpolation. For instance, let ℳ be the extension of the basic modal language with a difference operator [7]. Firstorder logic is the least expressive extension of ℳ with interpolation. These characterizations are subsequently used to derive new results about hybrid logic, relation algebra and the guarded fragment. 

A hybrid logic is obtained by adding to an ordinary modal logic further expressive power in the form of a second sort of propositional symbols called nominals and by adding socalled satisfaction operators. In this paper we consider hybridized versions of S5 (“the logic of everywhere”) and the modal logic of inequality (“the logic of elsewhere”). We give natural deduction systems for the logics and we prove functional completeness results. 