This paper investigates modular combinations of temporal logic systems. Four combination methods are described and studied with respect to the transfer of logical properties from the component one-dimensional temporal logics to the resulting combined two-dimensional temporal logic. Three basic logical properties are analyzed, namely soundness, completeness, and decidability. Each combination method comprises three submethods that combine the languages, the inference systems, and the semantics of two one-dimensional temporal logic systems, generating families of two-dimensional temporal languages with varying expressivity and varying (...) degrees of transfer of logical properties. The temporalization method and the independent combination method are shown to transfer all three basic logical properties. The method of full join of logic systems generates a considerably more expressive language but fails to transfer completeness and decidability in several cases. So a weaker method of restricted join is proposed and shown to transfer all three basic logical properties. (shrink)

This volume is dedicated to Leo Esakia's contributions to the theory of modal and intuitionistic systems. Consisting of 10 chapters, written by leading experts, this volume discusses Esakia’s original contributions and consequent developments that have helped to shape duality theory for modal and intuitionistic logics and to utilize it to obtain some major results in the area. Beginning with a chapter which explores Esakia duality for S4-algebras, the volume goes on to explore Esakia duality for Heyting algebras and its generalizations (...) to weak Heyting algebras and implicative semilattices. The book also dives into the Blok-Esakia theorem and provides an outline of the intuitionistic modal logic KM which is closely related to the Gödel-Löb provability logic GL. One chapter scrutinizes Esakia’s work interpreting modal diamond as the derivative of a topological space within the setting of point-free topology. The final chapter in the volume is dedicated to the derivational semantics of modal logic and other related issues. (shrink)

In this paper, we introduce a new fragment of the first-order temporal language, called the monodic fragment, in which all formulas beginning with a temporal operator have at most one free variable. We show that the satisfiability problem for monodic formulas in various linear time structures can be reduced to the satisfiability problem for a certain fragment of classical first-order logic. This reduction is then used to single out a number of decidable fragments of first-order temporal logics and of two-sorted (...) first-order logics in which one sort is intended for temporal reasoning. Besides standard first-order time structures, we consider also those that have only finite first-order domains, and extend the results mentioned above to temporal logics of finite domains. We prove decidability in three different ways: using decidability of monadic second-order logic over the intended flows of time, by an explicit analysis of structures with natural numbers time, and by a composition method that builds a model from pieces in finitely many steps. (shrink)

We show that the satisfiability problem for the monodic guarded, loosely guarded, and packed fragments of first-order temporal logic with equality is 2Exptime-complete for structures with arbitrary first-order domains, over linear time, dense linear time, rational number time, and some other classes of linear flows of time. We then show that for structures with finite first-order domains, these fragments are also 2Exptime-complete over real number time and hence over most of the commonly used linear flows of time, including the natural (...) numbers, integers, rationals, and any first-order definable class of linear flows of time. (shrink)

It is shown that the decision problem for the temporal logic with until and since connectives over real-numbers time is PSPACE-complete. This is the most practically useful dense time temporal logic.

We give a Hilbert style axiomatization for the set of formulas in the temporal language with Until and Since which are valid over the real number flow of time. The axiomatization, which is orthodox in the sense of only having the usual temporal rules of inference, is complete with respect to single formulas.