Mathematics & Physics 2016, 9(2), 149–157 УДК 510.643 Unification and Inference Rules in the Multi-modal Logic of Knowledge and Linear Time LTK Stepan I.Bashmakov∗ Institute of Mathematics and Computer Science Siberian Federal University Svobodny, 79, Krasnoyarsk, 660041 Russia Received 10.12.2015, received in revised form 10.01.2016, accepted 15.02.2016 We study unification of formulas in multi-modal LTK logic and give a syntactic description of all formulas which are non-unificable in this logic. <...> Passive inference rules are considered, it is shown that in LTK logic there is a finite basis for passive rules. <...> Introduction The research of unification for various logic systems is one of the most rapidly developing areas of modern mathematical logic. <...> For most of the non-classical logics (modal, pseudo-boolean, temporal, etc.), there are special dual equational theories of special algebraic systems, so their problems are reduced to the corresponding logical-unificational counterparts ( [5–7]). <...> Basic unificational problem can be viewed as a complex issue: whether the formula is to be transformed into a theorem after replacing the variables (keeping the same values of the coefficients parameters). <...> This issue was investigated and partly resolved (including V. V.Rybakov [8–10]), for intuitionistic and modal logics S4 and Grz. <...> Unification in intuitionistic logic and in propositional modal logic over the K4 investigated by S. Ghilardi [11–15] (with applications of projective algebra ideas and technology based on projective formulas). <...> In these works the problem of constructing the finite complete sets of unifiers was solved for the considered logic, efficient algorithms were found. <...> Such an approach proved to be a a useful and effective in dealing with the admissibility and the basis of admissible rules (Jerabek [16–18], Iemhoff, Metcalfe [19,20]). <...> Indeed, the existence of computable finite sets of unifiers follows directly solution of the admissibility problem. <...> Temporal logic is also very dynamic area of mathematical logic and computer science (including Gabbay и Hodkinson [21–23]). <...> In particular, LTL (linear temporal logic) has a significant application in the field of Computer Science (Manna, Pnueli [24, 25], Vardi [26, 27]). <...> Solving the problem of admissibility of rules <...>