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)

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.

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)

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)

We introduce a new way of defining metric temporal logic on a real-numbers flow of time. The idea is based on having semantics which allow us to refer to a single universal clock of arbitrary precision in order to impose metric constraints. This gives us a new metric temporal logic which is very expressive, is natural to use, can be applied in very general situations, affords a wide range of useful abbreviations and operators, has a PSPACE decision procedure, and has (...) the promise of being amenable to standard reasoning techniques. Thus it has many advantages over the existing metric temporal logics. We provide a decision procedure via conversion to a non-metric temporal logic, hence doing metric reasoning with no clocks. (shrink)

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.