This modern, advanced textbook reviews modal logic, a field which caught the attention of computer scientists in the late 1970's.

The Handbook of Modal Logic contains 20 articles, which collectively introduce contemporary modal logic, survey current research, and indicate the way in which the field is developing. The articles survey the field from a wide variety of perspectives: the underling theory is explored in depth, modern computational approaches are treated, and six major applications areas of modal logic (in Mathematics, Computer Science, Artificial Intelligence, Linguistics, Game Theory, and Philosophy) are surveyed. The book contains both well-written expository articles, suitable for beginners (...) approaching the subject for the first time, and advanced articles, which will help those already familiar with the field to deepen their expertise. Please visit: http://people.uleth.ca/~woods/RedSeriesPromo_WP/PubSLPR.html - Compact modal logic reference - Computational approaches fully discussed - Contemporary applications of modal logic covered in depth. (shrink)

Contemporary hybrid logic is based on the idea of using formulas as terms, an idea invented and explored by Arthur Prior in the mid-1960s. But Prior’s own work on hybrid logic remains largely undiscussed. This is unfortunate, since hybridisation played a role that was both central to and problematic for his philosophical views on tense. In this paper I introduce hybrid logic from a contemporary perspective, and then examine the role it played in Prior’s work.

Hybrid languages are expansions of propositional modal languages which can refer to worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work has focussed on a more constrained system called $\mathscr{H}$. We show in detail that $\mathscr{H}$ is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations and a syntactic characterization. The key result to emerge is that $\mathscr{H}$ corresponds to the fragment of first-order logic which is invariant for generated (...) submodels. We then show that $\mathscr{H}$ enjoys interpolation, provide counterexamples for its finite variable fragments, and show that weak interpolation holds for the sublanguage $\mathscr{H}$. Finally, we provide complexity results for $\mathscr{H}$ and other fragments and variants, and sharpen known undecidability results for $\mathscr{H}$. (shrink)

Hybrid languages have both modal and first-order 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 first-order language, that full first-order 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 (...) problems. (shrink)

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2 BASIC MODAL LOGIC . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.

How can computers distinguish the coherent from the unintelligible, recognize new information in a sentence, or draw inferences from a natural language passage? Computational semantics is an exciting new field that seeks answers to these questions, and this volume is the first textbook wholly devoted to this growing subdiscipline. The book explains the underlying theoretical issues and fundamental techniques for computing semantic representations for fragments of natural language. This volume will be an essential text for computer scientists, linguists, and anyone (...) interested in the development of computational semantics. (shrink)

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 (a decidable system with the same complexity as orthodox propositional modal logic) to the strong Priorean language (which offers full first-order expressivity).We show that hybrid logic offers a genuinely first-order 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 weaker languages, this requires the use of non-orthodox rules. We discuss these rules in detail and prove non-eliminability and eliminability results. We also show how another type of rule, which reflects the structure of the strong Priorean language, can be employed to give an even wider coverage of frame classes. We show that this deductive apparatus gets progressively simpler as we work our way up the expressivity hierarchy, and conclude the paper by showing that the approach transfers to first-order hybrid logic. (shrink)

On the 4th of December 1967, Hans Kamp sent his UCLA seminar notes on the logic of ‘now’ to Arthur N. Prior. Kamp’s two-dimensional analysis stimulated Prior to an intense burst of creativity in which he sought to integrate Kamp’s work into tense logic using a one-dimensional 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 (...) modal framework. With the aid of hybrid logic, Prior built a bridge from a two-dimensional UT calculus to a one-dimensional tense logic containing the ‘now’ operator J. Drawing on material from the Prior archive, and the paper “‘Now”’ that detailed Prior’s findings, we retell this story. We focus on Prior’s completeness conjecture for the hybrid system and the role played by temporal reference. (shrink)

We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret [email protected]_i$ in propositional and first-order hybrid logic. This means: interpret [email protected]_i\alpha _a$ , where $\alpha _a$ is an expression of any type $a$ , as an expression of type $a$ that (...) rigidly returns the value that $\alpha_a$ receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and (as is usual inhybrid logic) we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic. (shrink)

A modal logic is developed to deal with finite ordered binary trees a they are used in linguistics. A modal language is introduced with operators for the ‘mother of’, ‘first daughter of’ and ‘second daughter of’ relations together with their transitive reflexive closures. The relevant class of tree models is defined and three linguistic applications of this language are discussed: context free grammars, command relations, and trees decorated with feature structures. An axiomatic proof system is given for which completeness is (...) shown with respect to the class of finite ordered binary trees. A number of decidability results follow. (shrink)

We show that basic hybridization makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}[email protected]_i$\end{document} in propositional and first-order hybrid logic. This means: interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}[email protected]_i\alpha _a$\end{document}, where \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} (...) \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\alpha _a$\end{document} is an expression of any type \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$a$\end{document}, as an expression of type \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$a$\end{document} that rigidly returns the value that \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\alpha_a$\end{document} receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic. (shrink)

Quantified hybrid logic is quantified modal logic extended with apparatus for naming states and asserting that a formula is true at a named state. While interpolation and Beth's definability theorem fail in a number of well-known quantified modal logics , their counterparts in quantified hybrid logic have these properties. These are special cases of the main result of the paper: the quantified hybrid logic of any class of frames definable in the bounded fragment of first-order logic has the interpolation property, (...) irrespective of whether varying, constant, expanding, or contracting domains are assumed. (shrink)

Combining logics has become a rapidly expanding enterprise that is inspired mainly by concerns about modularity and the wish to join together tailor made logical tools into more powerful but still manageable ones. A natural question is whether it offers anything new over and above existing standard languages. By analysing a number of applications where combined logics arise, we argue that combined logics are a potentially valuable tool in applied logic, and that endorsements of standard languages often miss the point. (...) Using the history of quantified modal logic as our main example, we also show that the use of combined structures and logics is a recurring theme in the analysis of existing logical systems. (shrink)

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 re-entrancy, the ability to express generalisations, and the ability to express recursive constraints. Two main (...) techniques are used: either Kripke models with desirable properties are constructed, or modalities are used to simulate fragments of Propositional Dynamic Logic. Further possibilities for the application of modal logic in computational linguistics are noted. (shrink)

In this note we show that the classical modal technology of Sahlqvist formulas gives quick proofs of the completeness theorems in [8] (D. Gregory, Completeness and decidability results for some propositional modal logics containing "actually" operators, Journal of Philosophical Logic 30(1): 57-78, 2001) and vastly generalizes them. Moreover, as a corollary, interpolation theorems for the logics considered in [8] are obtained. We then compare Gregory's modal language enriched with an "actually" operator with the work of Arthur Prior now known under (...) the name of hybrid logic. This analysis relates the "actually" axioms to standard hybrid axioms, yields the decidability results in [8], and provides a number of complexity results. Finally, we use a bisimulation argument to show that the hybrid language is strictly more expressive than Gregory's language. (shrink)

This modern, advanced textbook reviews modal logic, a field which caught the attention of computer scientists in the late 1970's.

The title reflects my conviction that, viewed semantically,modal logic is fundamentally dialogical; this conviction is based on the key role played by the notion of bisimulation in modal model theory. But this dialogical conception of modal logic does not seem to apply to modal proof theory, which is notoriously messy. Nonetheless, by making use of ideas which trace back to Arthur Prior (notably the use of nominals, special proposition symbols which ‘name’ worlds) I will show how to lift the dialogical (...) conception to modal proof theory. I argue that this shift to hybrid logic has consequences for both modal and dialogical logic, and I discuss these in detail. (shrink)

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 well-known defect of Reichenbach’s tense schema, namely that it gives multiple representations to sentences in the future perfect and the future-in-the-past. It also makes it easy to define an iterative schema for tense that allows for multiple points of reference, a possibility noted (...) by Prior and demanded by Comrie, and we sketch how this schema can be generalized to a shift-and-restrict pattern in which special propositional symbols act as restrictors on the range of tense operators. (shrink)

This paper is about a special version of PDL, proposed by Marcus Kracht, for reasoning about sibling ordered trees. It has four basic programs corresponding to the child, parent, left- and right-sibling relations in such trees. The original motivation for this language is rooted in the field of model-theoretic syntax. Motivated by recent developments in the area of semi-structured data, and, especially, in the field of query languages for XML (eXtensible Markup Language) documents, we revisit the language. This renewed interest (...) comes with a special focus on complexity and expressivity aspects of the language, aspects that have so far largely been ignored. We survey and derive complexity results, and spend most of the paper on the most important open question concerning the language: what is its expressive power? We approach this question from two angles: Which first-order properties can be expressed? And which second-order properties? While we are still some way from definitive answers to these questions, we discuss two first-order fragments of the PDL language for ordered trees, and show how the language can be used to express some typical (second-order) problems, like the boolean circuit and the frontier problem. (shrink)

Este artigo canta uma canção — uma canção criada ao unir o trabalho de quatro grandes nomes na história da lógica: Hans Reichenbach, Arthur Prior, Richard Montague, e Leon Henkin. Embora a obra dos primeiros três desses autores tenha sido previamente combinada, acrescentar as ideias de Leon Henkin é o acréscimo requerido para fazer com que essa combinação funcione no nível lógico. Mas o presente trabalho não se concentra nas tecnicalidades subjacentes (que podem ser encontradas em Areces, Blackburn, Huertas, e (...) Manzano [no prelo]), e sim nos instrumentos subjacentes e no modo como trabalham em conjunto. Esperamos que o leitor fique tentado a cantar junto. DOI:10.5007/1808-1711.2011v15n2p225. (shrink)

Craig's interpolation lemma (if φ → ψ is valid, then φ → θ and θ → ψ are valid, for θ a formula constructed using only primitive symbols which occur both in φ and ψ) fails for many propositional and first order modal logics. The interpolation property is often regarded as a sign of well-matched syntax and semantics. Hybrid logicians claim that modal logic is missing important syntactic machinery, namely tools for referring to worlds, and that adding such machinery solves (...) many technical problems. The paper presents 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 elementary class of frames satisfying the property that a frame is in the class if and only if all its point-generated subframes are in the class. In addition, on the class of all frames, the basic algorithm is conservative: on purely modal input it computes interpolants in which the hybrid syntactic machinery does not occur. (shrink)

This is an exploratory paper about combining logics, combining theories and combining structures. Typically when one applies logic to such areas as computer science, artificial intelligence or linguistics, one encounters hybrid ontologies. The aim of this paper is to identify plausible strategies for coping with ontological richness.

In this paper back-and-forth structures are applied to the semantics of natural language. Back-and-forth structures consist of an event structure and an interval structure communicating via a relational link; transitions in the one structure correspond to transitions in the other. Such entities enable us to view temporal constructions (such as tense, aspect, and temporal connectives) as methods of moving systematically between information sources. We illustrate this with a treatment of the English present perfect, and progressive aspect, that draws on ideas (...) developed in Moens & Steedman (1988), and discuss the role of rich ontologies in formal semantics. (shrink)

This is an exploratory paper about combining logics, combining theories and combining structures. Typically when one applies logic to such areas as computer science, artificial intelligence or linguistics, one encounters hybrid ontologies. The aim of this paper is to identify plausible strategies for coping with ontological richness.

The papers you will find in this special issue of JoLLI develop letter and spirit of Turing’s original contributions. They do not lazily fall back into the same old sofa, but follow – or question – the inspiring ideas of a great man in the search for new, more precise, conclusions. It is refreshing to know that the fertile landscape created by Alan Turing remains a source of novel ideas.

In this article we discuss what constitutes a good choice of semantic representation, compare different approaches of constructing semantic representations for fragments of natural language, and give an overview of recent methods for employing inference engines for natural language understanding tasks.

With the rise of the internet and the proliferation of technology to gather and organize data, our era has been defined as "the information age." With the prominence of information as a research concept, there has arisen an increasing appreciation of the intertwined nature of fields such as logic, linguistics, and computer science that answer the questions about information and the ways it can be processed. The many research traditions do not agree about the exact nature of information. By bringing (...) together ideas from diverse perspectives, this book presents the emerging consensus about what a conclusive theory of information should be. The book provides an introduction to the topic, work on the underlying ideas, and technical research that pins down the richer notions of information from a mathematical point of view. The book contains contributions to a general theory of information, while also tackling specific problems from artificial intelligence, formal semantics, cognitive psychology, and the philosophy of mind. There is focus on the dynamics of information flow, and also a consideration of static approaches to information content; both quantitative and qualitative approaches are represented. (shrink)

This LNCS book is part of the FOLLI book series and constitutes the proceedings of the 7th International Workshop on Logic, Rationality, and Interaction, LORI 2019, held in Chongqing, China, in October 2019. The 31 papers presented in this book were carefully reviewed and selected from 56 submissions. They focus on the following topics: agency; argumentation and agreement; belief revision and belief merging; belief representation; cooperation; decision making and planning; natural language; philosophy and philosophical logic; and strategic reasoning.

Introduction to the Special Issue containing selected contributions to the conference "Formal Methods and Science in Philosophy IV", Inter-University Center, Dubrovnik, April 11-13, 2019.

In a study involving 62 Danish children with autism spectrum disorder, we obtained results showing that the mastery of linguistic recursion is a significant predictor of success in second-order false belief tasks. The same study also showed that the mastery of linguistic recursion was not significantly correlated with success in a task involving three heavily used Danish discourse particles. This calls for further explanation, as the reasoning involved in both types of tasks seems similar. In this paper, we discuss second-order (...) false belief reasoning, the reasoning underlying the use of the three Danish discourse particles, say what we know about them experimentally, and discuss what they do have in common. (shrink)