In the ordinary modal language, KD is the modal logic determined by the class of all serial frames. In this paper, we demonstrate that KD is nullary.

Epistemic logics are essential to the design of logical systems that capture elements of reasoning about knowledge. In this paper, we study the computability of unifiability and the unification types in several epistemic logics.

It is already known that unifiable formulas in normal modal logic |$\textbf {K}+\square ^{2}\bot $| are either finitary or unitary and unifiable formulas in normal modal logic |$\textbf {Alt}_{1}+\square ^{2}\bot $| are unitary. In this paper, we prove that for all |$d{\geq }3$|⁠, unifiable formulas in normal modal logic |$\textbf {K}+\square ^{d}\bot $| are either finitary or unitary and unifiable formulas in normal modal logic |$\textbf {Alt}_{1}+\square ^{d}\bot $| are unitary.

The unification problem in a normal modal logic is to determine, given a formula.

We study quasi-characterizing inference rules (this notion was introduced into consideration by A. Citkin (1977). The main result of our paper is a complete description of all self-admissible quasi-characterizing inference rules. It is shown that a quasi-characterizing rule is self-admissible iff the frame of the algebra generating this rule is not rigid. We also prove that self-admissible rules are always admissible in canonical, in a sense, logics S4 or IPC regarding the type of algebra generating rules.

ABSTRACT We1 study unification of formulas in modal logics and consider logics which are equivalent w.r.t. unification of formulas. A criteria is given for equivalence w.r.t. unification via existence or persistent formulas. A complete syntactic description of all formulas which are non-unifiable in wide classes of modal logics is given. Passive inference rules are considered, it is shown that in any modal logic over D4 there is a finite basis for passive rules.

Contact Logics provide a natural framework for representing and reasoning about regions in several areas of computer science. In this paper, we focus our attention on reasoning methods for Contact Logics and address the satisfiability problem and the unifiability problem. Firstly, we give sound and complete tableaux-based decision procedures in Contact Logics and we obtain new results about the decidability/complexity of the satisfiability problem in these logics. Secondly, we address the computability of the unifiability problem in Contact Logics and we (...) obtain new results about the unification type of the unifiability problem in these logics. (shrink)

In [5] Phillips proved that one can obtain the additive group of any nonstandard model *ℤ of the ring ℤ of integers by using a linear mod 1 function h : F ℚ, where F is the α-dimensional vector space over ℚ when α is the cardinality of *ℤ. In this connection it arises the question whether there are linear mod 1 functions which are neither addition nor quasi-linear. We prove that this is the case.