English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The research of unification for various logic systems is one of the most rapidly developing areas of modern mathematical logic. Arisen in the field of Computer Science, primarily in the form of a question about the possibility to transform two different terms in syntactically equivalent by replacing the variables of certain other terms ( [1,2]), from the time the task has changed course on the study of semantic equivalence ( [3, 4]). 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 in the LTL was proposed by Rybakov [28], basis of admissible

Unification and Inference Rules in the Multi-modal Logic of Knowledge and Linear Time LTK