This paper introduces and studies a new type of logical construction, which allows to combine various non-classical propositional logics with the temporal or modal background. The possible candidates include a number of epistemic, multi-agent, deontological and other well-studied logics. In this construction, that we call refinement, the Kripke structure of a chosen Kripke complete logic is imposed on clusters of the background transitive frame. Refinements fit in a wider framework of fibred logics, while having some unique features. First of all, (...) when applied to classes of frames of Kripke complete logics, refinement preserves good meta-logical properties of constituent logics, in contrast with the well-known products of logics. Another advantage of refinements is that they allow for augmented languages of considerable expressive power, while preserving good meta-logical and semantical properties. In particular we show that refinement of logics preserves the effective finite model property and decidability for a wide class of constituent logics. (shrink)

The problem of unification in a normal modal logic $L$ can be defined as follows: given a formula $\varphi$, determine whether there exists a substitution $\sigma$ such that $\sigma $ is in $L$. In this paper, we prove that for several non-symmetric non-transitive modal logics, there exists unifiable formulas that possess no minimal complete set of unifiers.

While specifications and verifications of concurrent systems employ Linear Temporal Logic , it is increasingly likely that logical consequence in image will be used in the description of computations and parallel reasoning. Our paper considers logical consequence in the standard image with temporal operations image and image . The prime result is an algorithm recognizing consecutions admissible in image, so we prove that image is decidable w.r.t. admissible inference rules. As a consequence we obtain algorithms verifying the validity of consecutions (...) in image and solving the satisfiability problem. We start by a simple reduction of logical consecutions of image to equivalent ones in the reduced normal form . Then we apply a semantic technique based on image-Kripke structures with formula definable subsets. This yields necessary and sufficient conditions for a consecution to be not admissible in image. These conditions lead to an algorithm which recognizes consecutions admissible in image by verifying the validity of consecutions in special finite Kripke structures of size square polynomial in reduced normal forms of the consecutions. As a consequence, this also solves the satisfiability problem for image. (shrink)

The paper deals with a temporal multi-agent logic TMAZ, which imitates taking of decisions based on agents' access to knowledge by their interaction. The interaction is modelled by possible communication channels between agents in special temporal Kripke/hintikka-like models. The logic TMAZ distinguishes local and global decisions-making. TMAZ is based on temporal Kripke/hintikka models with agents' accessibility relations defined on states of all possible time clusters C(i) (where indexes i range over all integer numbers Z). The main result provides a decision (...) algorithm for TMAZ (so, we prove that TMAZ is decidable). This algorithm also solves the satisfiability problem. In the final part of the paper, we consider the admissibility problem for inference rules in TMAZ, and show that this problem is decidable for TMAZ as well. (shrink)

The paper studies the logic TL(NBox+-wC) – logic of discrete linear time with current time point clusters. Its language uses modalities Diamond+ (possible in future) and Diamond- (possible in past) and special temporal operations, – Box+w (weakly necessary in future) and Box-w (weakly necessary in past). We proceed by developing an algorithm recognizing theorems of TL(NBox+-wC), so we prove that TL(NBox+-wC) is decidable. The algorithm is based on reduction of formulas to inference rules and converting the rules in special reduced (...) normal form, and, then, on checking validity of such rules in models of singleexponential size in the rules. Also we consider the admissibility problem for TL(NBox+-wC) and show how to reduce the problem for admissibility to the decidability of TL(NBox+-wC) itself using definable universal modalities. (shrink)