This issue presents the Proceedings of the International Conference ‘Computer Science Applications of Modal Logic’ held in Moscow, September 5–9, 2005. The conference was organized by the French–Russian Mathematical Laboratory Poncelet (UMI 2615) as a part of cooperative programs between CNRS (the French National Centre for Scienctific Research) and the Independent University of Moscow, and between NWO (the Netherlands Organization for Scientific Research) and Russian Academy of Sciences. The event was also sponsored by Russian Foundation for Basic Research (RFBR), Moscow Centre for Continuous Mathematical Education (MCCME) and Steklov Mathematical Institute. The conference involved about 30 researchers in modal logic from different countries (Russia, France, Holland, USA, UK, Bulgaria and South Africa), many of them quite young. The talks covered different subjects of applied modal logic (in a broad sense), including temporal logics, dynamic logics, logics of proofs, epistemic logics, action logics, verification, complexity, many-dimensional modal logics, description logics, geometrical and topological modal logics, first-order modal and intermediate logics, logic and games. The readers of the presented articles may have a good impression of the large variety of topics discussed at the conference—but unfortunately, not all interesting talks are reflected here. (The collection of abstracts can be found at http://www.mccme.ru/poncelet).

The paper studies modal logics of Kripke frames, in which possible worlds are regions in space with natural accessibility relations. These logics are also interpreted as relativistic temporal logics. Together with an overview, we prove some new results on completeness, decidability, complexity, and finite axiomatizability.

The interest in fragments of predicate logics is motivated by the well-known fact that full classical predicate calculus is undecidable (cf. Church [1936]). So it is desirable to find decidable fragments which are in some sense “maximal”, i.e., which become undecidable if they are “slightly” extended. Or, alternatively, we can look for “minimal” undecidable fragments and try to identify the vague boundary between decidability and undecidability. A great deal of work in this area concerning mainly classical logic has been done since the thirties. We will not give a complete review of decidability and undecidability results in classical logic, referring the reader to existing monographs (cf. Suranyi [1959], Lewis [1979], and Dreben, Goldfarb [1979]). A short summary can also be found in the well-known book Church [1956]. Let us recall only several facts. Herein we will consider only logics without functional symbols, constants, and equality. (C1) The fragment of the classical logic with only monadic predicate letters is decidable (cf. Behmann [1922]). (C2) The fragment of the classical logic with a single binary predicate letter is undecidable. (This is a consequence of Gödel [1933].) (C3) The fragment of the classical logic with a single individual variable is decidable; in fact it is equivalent to Lewis S5 (cf. Wajsberg [1933]). (C4) The fragment of the classical logic with two individual variables is decidable (Segerberg [1973] contains a proof using modal logic; Scott [1962] and Mortimer [1975] give traditional proofs.) (C5) The fragment of the classical logic with three individual variables and binary predicate letters is undecidable (cf. Surańyi [1943]). In fact this paper considers formulas of the following type φ,ψ being quantifier-free and the set of binary predicate letters which can appear in φ or ψ being fixed and finite.