\documentclass[11pt,reqno]{amsart}
\usepackage[cp1251]{inputenc}
\usepackage[english,russian]{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{graphicx}
\usepackage{xcolor}
\usepackage[colorlinks]{hyperref}


\usepackage{titlesec}
\titlespacing{\section}{0pt}{2.5ex}{1.5ex}
\titlespacing{\subsection}{0pt}{1.5ex}{1ex}
\titlespacing{\subsubsection}{0pt}{1.5ex}{1ex}
\titleformat{\section}{\large\bfseries\centering}{\thesection}{1em}{}
\titleformat{\subsection}[runin]{\bfseries}{\thesubsection.}{0.5em}{}[.\mbox{\ }]
\titleformat{\subsubsection}[runin]{\bfseries}{\thesubsubsection.}{0.4em}{}[.\mbox{\ }]



%%%%%---------- ORCiD
\newcommand\orcidicon[1]{\href{https://orcid.org/#1}{\includegraphics[scale=0.02]{orcid.pdf}}}

\def\udcs{510.6, 519.7} %Здесь автор определяет УДК своей работы
\def\mscs{03B45,03B70} %Здесь автор определяет классификаторы AMS своей работы
\setcounter{page}{144}

\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}
\newtheorem{proposition}{Proposition}


\definecolor{myblue}{rgb}{0.03, 0.27, 0.79}

\hypersetup{linkcolor=blue,filecolor=black,urlcolor=blue, citecolor=blue}

\def\logo{\textcolor{blue}{{\bf\Huge S\raisebox{0.2ex}{\hspace{0.55ex}\raisebox{0.05ex}e\hspace{-1.65ex}$\bigcirc$}MR}}}

\def\semrtop
     {
  \vbox{
     \noindent\logo \hspace{-3mm}  \parbox{12cm}{     \begin{center}
     {\LARGE \textsf{Siberian Electronic}} \\[2mm]
     {\LARGE \textsf{Mathematical Reports}} \\[2mm]
     {\Large \textsf{Siberian Electronic Mathematical Reports}} \\[1mm]
     {\Large\tt{\textcolor{blue}{http://semr.math.nsc.ru}}}\\[1mm]
     \raisebox{1ex}{ISSN 1813-3304 }
     \vspace*{-3mm}
%     {\small Институт математики им. С.Л.Соболева СО РАН}\\[-1mm]
%     {\small Sobolev Institute of Mathematics SB RAS}
     \end{center}
}
     \vspace{-1mm}
     \noindent
      \begin{tabular}{c}
     \hphantom{aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa!} \\
     \hline\hline
     \end{tabular}

     \vspace{3mm}
     {\flushleft\it Том 20, № 2, стр. 144--145 (2023) \hspace{\fill}{\rm\small УДК \udcs \hspace{-4mm}}}
     \newline
        {\rm\small \textcolor{blue}{https://doi.org/10.33048/semi.2023.20.???}}\hphantom{aaaaaaaaaaaaaaaaaaaaaaaa\;}{\rm\small MSC\ \ \mscs }
  }%\vbox
}


\newcommand{\nn}{{\it N}}

\newcommand{\pp}{{{\bf N^{-1}}}}


\newcommand{\uu}{{{\it U}}}

\newcommand{\bb}{{{\bf B}}}


\newcommand{\ga}{\alpha}
\newcommand{\ca}{{\cal A}}
\newcommand{\gb}{\beta}
\newcommand{\cb}{{\cal B}}
\newcommand{\grg}{\gamma}
\newcommand{\cg}{{\cal G}}
\newcommand{\gd}{\delta}
\newcommand{\cd}{{\cal D}}
\newcommand{\gl}{\lambda}
\newcommand{\cl}{{\cal L}}
\newcommand{\gr}{\rho}
\newcommand{\gx}{\xi}
\newcommand{\ppp}{\varphi}
\newcommand{\cf}{{\cal F}}

\newcommand{\gm}{\mu}
\newcommand{\Gg}{\Gamma}
\newcommand{\Gd}{\Delta}
\newcommand{\goa}{{\goth A}}
\newcommand{\gob}{\goth B}
\newcommand{\gom}{\goth M}
\newcommand{\god}{\goth D}
\newcommand{\gon}{\goth N}
\newcommand{\gof}{\goth F}
\newcommand{\ggf}{{\goth F}(\gl)}
%\newcommand{\cf}{{\cal F}or}

\newcommand{\cc}{{\cal C}}
%\newcommand{\cff}{{\cal F}}


\newcommand{\cs}{{\cal S}}
\newcommand{\cq}{{\cal Q}}
\newcommand{\ck}{{\cal K}}
\newcommand{\ce}{{\cal E}}

\newcommand{\cw}{{\cal W}}
\newcommand{\cx}{{\cal X}}
\newcommand{\cz}{{\cal N}}
\newcommand{\hc}{{\cal H}}
\newcommand{\cp}{{\cal P}}
\newcommand{\cy}{{\cal Y}}
\newcommand{\cln}{{\cal N}}
\newcommand{\cu}{{\cal U}}
\newcommand{\vf}{{\varphi}}
\newcommand{\vp}{{\psi}}
\newcommand{\cas}{{\cal A}{\cal S}}
\newcommand{\cma}{{\cal M}}
\newcommand{\ty}{{\cl_{t,y}(\cz)}}
\newcommand{\ccc}{\mathrm{\bf c_{nf}}}
%\newcommand{\llll}{LTL^{\mbox{\tiny U,N}}({\cal N})}
\newcommand{\llll}{{\cal LT \hspace*{-0.05cm}L}}
\newcommand{\nnn}{{\cal N}}
\newcommand{\sss}{{{\bf S}}}
\newcommand{\zzz}{{\cal LT \hspace*{-0.05cm}L}_K(Z)}
\newcommand{\zz}{{{\cal Z}_C}}

\newcommand{\ms}[0]

{\medskip}
\newcommand{\ii}[0]
{\rightarrow}

\newcommand{\ri}[0]
{\mbox{$\Rightarrow$}}

\newcommand{\lri}[0]
{\mbox{$\Leftrightarrow$}}

\newcommand{\lr}[0]
{\mbox{$\Longleftrightarrow$}}

\newcommand{\eq}[2]{
\begin{equation}
#1 \label{#2}
\end{equation}}

\newcommand{\ci}[1]{\cite{#1}}


\newcommand{\pr}{{\sl Proof}}



\newcommand{\cpc}[0]{\mbox{PC}}
\newcommand{\cpcc}[0]{\mbox{PrC}}

\newcommand{\zk}[0]{\mbox{K}}
\newcommand{\zsf}[0]{\mbox{S4}}
\newcommand{\zkf}[0]{\mbox{K4}}
\newcommand{\zsv}[0]{\mbox{S5}}
\newcommand{\zh}[0]{\mbox{H}}
\newcommand{\zi}[0]{\mbox{Int}}
\newcommand{\zkc}[0]{\mbox{KC}}
\newcommand{\zkp}[0]{\mbox{KP}}
\newcommand{\zlc}[0]{\mbox{LC}}
\newcommand{\zt}[0]{\mbox{T}}
\newcommand{\zsfr}[0]{\mbox{S4.3}}
\newcommand{\zsfw}[0]{\mbox{S4.2}}
\newcommand{\zsfn}[0]{\mbox{S4.1}}

\newcommand{\ar}[1]{
\[ \begin{array} #1 \end{array}\]}

\newcommand{\mm}[2]{\langle #1, #2 \rangle}

\newcommand{\mk}[3]{\langle #1, #2, #3 \rangle}



\newcommand{\dd}[0]{
\rule{1.5mm}{1.5mm}}



\newcommand{\vv}[0]{
\unitlength=1mm \linethickness{0.5pt} \protect{
\begin{picture}(4.40,4.00)
\put(1.2,-0.4){\line(0,1){3.1}} \put(2.1,-0.4){\line(0,1){3.1}}
\put(2.1,1.1){\line(1,0){2.0}}
\end{picture}\hspace*{0.3mm}}}


\newcommand{\nvv}[0]{
\unitlength=1mm \linethickness{0.5pt} \protect{
\begin{picture}(4.40,4.00)
\put(2.1,-0.4){\line(0,1){3.1}} \put(2.1,1.2){\line(1,0){2.0}}
\protect{ \put(0.6,-0.5){\line(1,1){3.6}}}
\end{picture}\hspace*{0.3mm}
} }




\begin{document}
\renewcommand{\refname}{References}


\thispagestyle{empty}

\title[\sc Non-linear Temporal Logic]{Non-linear Temporal Logic, Admissibility for Rules and Almost-Projective Formulas}
\author[V/ V/ Rybakov]{{\bf \large \textsc{V.V.Rybakov}}\protect\orcidicon{0000-0001-8827-2630}\\ \\
%\textit{Представлено} \textsc{П.П. Петровым}
%\textit{(заполняется редактором)}
}%
\address{Vladimir Vladimirovich  Rybakov   % Контактные данные всех авторов и место работы указываются только на английском языке
\newline\hphantom{iii} Siberian Federal University,
\newline\hphantom{iii} av. Svobodnui 79,
\newline\hphantom{iii} 630090, Krasnoyarsk, Russia}%
\email{\textcolor{blue}{vladimir\_rybakov@mail.ru}}%

%\thanks{\sc Ivanov, I.I.,
%n some problems of commutative algebra}
%\thanks{\copyright \ 2023 Иванов И.И}
%\thanks{\rm Работа поддержана РФФИ (грант 03-01-11111)}
%\thanks{\it Поступила 1 января 2023 г., опубликована 31 декабря 2023 г.}%


\semrtop \vspace{1cm}
\maketitle {\small
%\begin{quote}



%\noindent{\bf Abstract:} In this paper\footnote{This work was supported by the Russian Science Foundation under %grant
%no. 23-21-00213, https://rscf.ru/project/23-21-00213/ and by the Russian Science Foundation under
%grant no. 25-21-20011, https://rscf.ru/project/25-21-20011}
%we study
 %admissibility problem for non-linear temporal logic $L$.
%We consider a special generalization of projective formulas.
%Using this technique
 %we find algorithm computing most general unifier for
%any given unifiable in $L$ formula. Logic $L$ is generated by family of all closed temporal models with compression %property.
%Based on prepared technique, we prove that the admissibility problem and unification problem for $L$ are decidable.

%\end{abstract}




\bigskip

%\section{Introduction}

%\begin{document}
\maketitle



\medskip

ABSTRACT. {\it
In this paper\footnote{This work was supported by the Russian Science Foundation under grant
no. 23-21-00213, https://rscf.ru/project/23-21-00213/ and by the Russian Science Foundation under
grant no. 25-21-20011, https://rscf.ru/project/25-21-20011}
we study
 admissibility problem for non-linear temporal logic $L$.
We consider a special generalization of projective formulas.
Using this technique
 we find algorithm computing most general unifier for
any given unifiable in $L$ formula. Logic $L$ is generated by family of all closed temporal models with compression property.
Based on prepared technique, we prove that the admissibility problem and unification problem for $L$ are decidable.}

\medskip

\bigskip

{\bf Keywords:} temporal logic, unification, admissibility problem,

\hspace*{0.0cm} computation of unifiers, projective formulas, admissible rules


\bigskip



\section{Introduction, background}

In logic and computer science, specifically automated reasoning, unification is an algorithmic process of solving equations between symbolic expressions. This technique often
 used in automated deduction, optimization programs  and
 pure mathematical logic (cf.
 Robinson \cite{rob1}, Knuth et al \cite{kb2},
 Baader and Snyder \cite{kb3},  Baader and Ghilardi \cite{bg4}). In particular it is a prominent instrument for
  verification  admissibility for inference rules. For example,
Harvey Friedman problem about recognoscing  admissibility for inference rules
in the intuitionistic propositional logic INT has close connection  with properties of unification (the Friedman problem was solved by V.Rybakov (in 1984, cf. for reference and history the book \cite{r10}). And later in 1997
Silvio Ghilardi  \cite{g11,g13}
found another solution of admissibility problem  by usage projective  formulas
and unification
(cf. S.~Ghilardi \cite{g11,g13,g14}). This view on admissible rules was developed longer by several authors
 (cf. eg.  Jer\'abek \cite{je16,je17}, Iemhoff, Metcalfe \cite{ie19f,ie20f}, Balbiani at all  \cite{ba21,ba22}, Bashmakov at all \cite{bs23}). W.r.t.
admissibility, a generalization of this problem on inference rules which may contains parameters (looks the same as coefficients in algebraic equations) is more interesting and more complicated.
This problem was solved by
Rybakov \cite{r8,r9,r10}
 for intuitionistic logic and modal logics $S4$ and $Grz$.

 We will work in this paper with a  variation of temporal logic and unification. As well known in mathematical logic and philosophy, temporal logic is a mathematical  symbolism for representing, and reasoning about events
 qualified in terms of time.
 In literature, temporal logic sometimes used to refer to tense logic, as -- a modal logic-based system of temporal logic which was introduced by Arthur Prior in the late 1950s. It has been further developed and applied in computer scientists, notably by Amir Pnueli, and other logicians (cf. e.g. Gabbay at al
 \cite{ga24,ga25}), cf. \cite{va30,r32,r34}).


Linear modal logic may be seen as
 linear temporal logic (logic with linear time). Studying it
 Dzik and Wojtylak \cite{dw36} proved that any formula unifiable in the linear modal logic $S4.3$ is projective, which gives direct solution of admissibility problem for $S4.3$.
(Ideas similar to projectivity for linear modal and intuitionistic logics
were suggested already in A. Wroґnski \cite{wr37,wr38}).


At the same time,
 progress for admissibility problem in temporal logic itself was rather not so successful, many problems remain open. Even until now the admissibility problem was not solved  for none-linear temporal logic with transitive (accessibility by time) relation.
In this paper we consider admissibility problem in some such non-linear temporal logic. We assume that $L$ is generated by family of all possible temporal models which are closed and have the compression property.
We consider a modification of projective formulas and by it we find algorithm computing most general unifier for
any given unifiable in $L$ formula. So we prove that unifiability problem and admissibility problems for such logic $L$
are decidable.







\section{A very few known definitions and denotation}

We start from definition  the syntax for our temporal logic.
It contains the
 set $Prop$ of propositional letters and Boolean logical operations.

 As for additional temporal logical operations we have a choice for using and fixing notation.
 First, paying respect to Prior for his invention,  we may consider only
  Prior's choice for operations: unary logical operation $G$ (means -- it always will  be true)  and unary logical operation $H$ (it always was true in past).  So for a formula $\varphi$,
  $G\varphi$ is meant as: always in future $\varphi$ will be always true,  $H\varphi$ says that always in past $\varphi$ was true.

  Second way, besides we may use only  modified standard modal logical operations $\Box^+$ (for future) and $\Box^{-}$ {for past} and they may be expressed
    by standard mentioned temporal ones: $\Box^+ \varphi :=  G \varphi$, $\Box^{-}\varphi :=  H  \varphi$. And  wise versa $G \varphi := \Box^{+} \varphi$, $H \varphi = \Box^{-} \varphi$.
    Later we will prefer to use only  $\Box^{+}$ and  $\Box^{-}$ as additional temporal operations.


Now we briefly recall (well known) definitions for semantic of modal and temporal bi-models.
Standard semantics for modal propositional logics consists of frames $F :=
 \langle W, R \rangle$ (that are sets $W$ of possible states (worlds)
with a binary accessibility relation $R$ on $W$; so, if $a,b \in W$ and $a R b$ we say that $b$ is accessible from $a$). Models are obtained from the frames by introduction valuations $V$ for some chosen sets of propositional letters
 $Prop$.
  So, for any
 $p\in Prop$, $V(p)\subseteq W$, $V(p)$ is the
 set of all $w$ from $W$
 where $p$ is  true (w.r.t. $V$).
 The triple $M := \langle W, R, V
 \rangle$ is said to be a Kripke model.

 \smallskip

For any Kripke model
 $M$,
 the truth values can
be extended from propositions of $Prop$ to arbitrary (bi-modal) formulas
 as follows:

\smallskip

$ \forall p\in Prop \ (M,a)\vv_V p \ \lri  a\in W \wedge \ a\in V(p);$

\smallskip

$ (M,a)\vv_V (\varphi\wedge \psi) \ \lri
(M,a)\vv_V \varphi \ \wedge \
(M,a)\vv_V \psi;$

\smallskip


$ (M,a)\vv_V (\varphi\vee \psi) \ \lri
(M,a)\vv_V \varphi \ \vee \
(M,a)\vv_V \psi;$


\smallskip

$ (M,a)\vv_V \neg \varphi \ \lri not [(M,a)\vv_V \varphi]  ;$

\smallskip



$ (M,a)\vv_V \Box^{+} \varphi \ \lri \forall b
[(a \ R \ b) \ri (M,b)\vv_V \varphi]  ;$

\smallskip


$ (M,a)\vv_V \Box^- \varphi \ \lri \forall b
[(b\ R \ a) \ri (M,b)\vv_V \varphi]  .$

\medskip


 { For a Kripke model $M:=\langle W, R,V  \rangle$ and a formula $\varphi$ with letters from the domain of $V$,
 $\varphi$ is valid in $M$ (denotation -- $M\vv \varphi$) if, \ for any
$b$ of $W$,
 the formula $\varphi$ is true at $b$ (denotation: $(M,b)\vv_V
\varphi)$.}

\begin{definition} {\em For a given class of frames $K$, the temporal (bi-modal) logic generated by $K$ is the set of all temporal formulas
which are true at any state of any model obtained from any frame from $K$ by introduction of any possible valuation of propositional letters; notation $L = L(K)$.
}
\end{definition}

Any modal logic is simply a particular case of bi-modal logic
when we use only one modal operation $\Box$ (as $\Box^+$) instead two ones:
$\Box^{+}$ and  $\Box^{-}$.


In this paper we consider only frames with reflexive and transitive accessibility relations $R$.
Logic $L(K)$ itself is decidable if for any formula we may compute if $\varphi \in  L(K)$.
A formula $\varphi$ is {\em satisfiable} in $L(K)$  if there is a model $M$ constructed on a frame from $K$, where
$\varphi$ is true at some its state.





\section{A modification for definition of projective formulas}
First we briefly recall the known standard definitions in order to show how our  extension works towards standard projective formulas. Our comments below are exactly the same for any modal or bi-modal logic.
Let $For$ be the set of all formulas,
 let $P$ be a set of letters. A mapping $\varepsilon$  of $P$ into
$For$ is said to be a
substitution for $P$.
That substitution $\varepsilon$ can be extended to
the set of all formulas in letters from $P$ by $\varepsilon
(\varphi(x_1, \dots , x_n)) := \varphi(\varepsilon(x_1), \dots ,
\varepsilon(x_n))$. That  is similar for all logics.



\begin{definition} \label{lu1m3}
A formula $\varphi$ is unifiable in a logic $L$ if there is a substitution
$\varepsilon$ which is called a unifier for $\varphi$ such that $
\varepsilon(\varphi) \in L$.
\end{definition}

That is $\varepsilon(\varphi)$ is the result of substitution formulas $\varepsilon (x_i)$
in the formula $\varphi$ instead any propositional letter $x_i$ occurring in $\varphi$.
 {\it
A unifier $\varepsilon$ (for a formula $\varphi$ in a logic $L$) is more
general than a unifier $\varepsilon_1$ iff there is a substitution
$\delta$ such that for any letter $x$, $[\varepsilon_1(x) \equiv
\delta(\varepsilon(x))] \in L$. }
 A set of unifiers $CU$ for a given formula $\varphi$ in a logic $L$ is a complete set of
unifiers, if the following holds. For any unifier
$\sigma$ for $\varphi$ in $L$, there is a unifier $\sigma_1$ from $CU$, where $\sigma_1$ is more general than
$\sigma$.



If a logic $L$ is decidable, usually  to check the unifiability a formula in $L$
is (theoretically, not computationally)  an easy task: it is sufficient
to use only ground substitutions: mappings of propositional letters in the set
$\{\bot, \top\}$. But the problem - how to find all unifiers - all solving substitutions - is not easy at all.
Now we recall the standard definition of projective formulas for modal logics.

\begin{definition} A formula $\varphi$ is said to be projective in a logic $L$
if the following holds. There is a substitution $\sigma$ (which is called
projective substitution) which is an unifier for $\varphi$ such that $\Box \varphi \ii [ x_i \equiv \sigma (x_i)] \in L$ for any letter $x_i$ from $\varphi$.
\end{definition}

The use of projective formulas for modal logics comes from the following statement.

\begin{lemma} \label{l1sss} If a substitution $\sigma_p$ is projective
  for a formula $\varphi$  in a modal logic $L$, then $\{\sigma_p\}$ is a complete set of unifiers for $\varphi$ (i.e. $\sigma_p $ is most general unifier).
\end{lemma}

\pr. Indeed, let $\sigma$ be a unifier for $\varphi$ in $L$.
Since we assume $\sigma_p$ is projective for $\varphi$ in $L$, we have
$\Box \varphi \ii [x_i \equiv \sigma_p(x_i)] \in L$ for any letter $x_i$ from $\varphi$. Acting by $\sigma$ on the formula above we get
$\sigma(\Box \varphi) \ii [\sigma(x_i) \equiv \sigma (\sigma_p (x_i))] \in L $,
that is $\sigma(x_i) \equiv \sigma (\sigma_p (x_i)) \in L $. Q.E.D.

\medskip

It works very well for linear modal logics for finding most general unifiers, but for not-linear ones and moreover for temporal logics
that approach cannot be applied directly .
Also recall that not all unifiable formulas are projective.
 Recall (without a proof) a known result concerning the linear temporal logic $L$ (on the set of all natural numbers as the generating frame).


Example (cf. eg. \cite{br31}).
 {\it Formula $\varphi =\Box(\Box x\vee (\neg x\wedge \nn \Box x))$
  is unifiable in $L$ but not projective.}




\smallskip

In this our  paper we study an non-linear temporal logics with aim to sole problem of  computability for admissible rules and for
finding most general unifiers. For this we introduce some restriction on temporal logics under our consideration.

Note that we do not consider in our this paper temporal logics with operation {\it until} (or {\it since})  because the logic is not linear and so there is no way to define correctly the rules for computation {\it until} (or {\it since}).
As noted already,
a temporal frame is
a pair $\langle W, R\rangle $, where $W$ is a set (temporal states) and $R$ is a binary relation on $W$ (accessibility for states,
$a R b$ means that the state $b$ is accessible form state $a$).


We fix that since now, by definition, the relations $R$ are always reflexive and transitive.

To simplify writings we write $a R^+b$ for $a R b$ (with meaning $b$ is future state for $a$) and $a R^-b$ for $b R a$  (with meaning $b$ is past state for $a$).

 Now we turn to our modification of definition for projective formulas. We need



%\end{document}


\begin{definition} \label{lu1m3} {\it
We say that a temporal frame $\langle W, R \rangle$ is closed if for any two states $a,b \in W$ there are states
$a_1,b_1,a_2, b_2,
 \ . . . \ a_i,b_i,\ ... \  a_k,b_k \in W$ such that $a=a_1$, $b = b_k$, and


 \[ a_1 R^+ b_1, b_1  R^{-}  a_2, a_2  R^{+}  b_2, \
 \ . . . \ , a_i R^+ b_i, b_i R^- a_{i+1}, \ ... \ , a_k R^+ b_k.\]
 }
 \end{definition}


 In this case we will say that there is an zig-zag path in $W$ from $a$ to $b$ of length $k$.


\begin{definition} \label{lu1m} {\it
Let $ k \in N$. We say a temporal logic $L$ has $k$-zig-zag compression  if $L$ is generated by a family Kripke frames
$\langle W, R  \rangle$,
such that for any such $\langle W, R  \rangle$ the following holds.

If for any $a_1,b_1,a_2, b_2,
 \ . . . \ a_i,b_i,\ ... \  a_n,b_n$ from  $W$ with $n \geq k+1$ and

 \[ a_1 R^+ b_1, b_1  R^{-}  a_2, a_2  R^{+}  b_2, \
 \ . . . \ , a_i R^+ b_i, b_i R^- a_{i+1}, \ ... \ , a_n R^+ b_n.\]


there are
    $c_1,  d_1,  \ . . . \ c_i, d_i, \ ... \  c_m, d_m \in W $
 such that

 \[ c_1 R^+ d_1,  d_1 R^{-}  c_2,  c_2 R^{+}  d_2,  \
 \ . . . \  , c_i R^+ d_i , d_i R^- c_{i+1}\ ... \  c_{m}  R^+ d_m,\]

 and $a_1 = c_1, b_n = d_m$,   where $m < k+1$.
}
\end{definition}
That is, if there is a zig-zag path from $a_1$ to $b_n$ inside $W$ of, say, --  zig-zag  length $n$, which is bigger as $k$,
then there is
 a zig-zag path from $a_1$ to $b_n$ inside $W$ of length at most $k$.
  Recall now definition of main object of our research - admissibility of inference rules.


\begin{definition} Let $\varphi_1, \dots, \varphi_n,  \psi$ be some formulas. Inference rule compound from this formulas is the expression
 $\varphi_1, \dots \varphi_n /  \psi$. It said to be admissible in a logic $L$ iff for any substitution
 $\epsilon$ if $\epsilon(\varphi_1) \in L, \dots ,  \epsilon(\varphi_n) \in L$ then $ \epsilon(\psi) \in L$.
  \end{definition}



\section{Results on Decidability}

We consider now below only non-linear temporal logic $L$ which is generated by all closed temporal  frames with
 $k$-zig-zag compression (that is L = L(K)). It is clear that a formula $\varphi$ is unifiable in $L$ iff $\varphi$ is true in one element
reflexive frame. We turn now to find a complete set of unifiers.

For a formula $\varphi$ and $m \in N$, $ \ [\Box^+\Box^-]^{m} \varphi \ $  denotes the formula

$(\Box^+\Box^-)( \Box^+\Box^- ) ...   (\Box^+\Box^-) (\Box^+\Box^-) \varphi $
where $(\Box^+\Box^-)$ is taken $m$ times.



\begin{theorem} \label{mntAab} For (non-linear) temporal logic $L$ generated by all closed temporal  frames with
 $k$-zig-zag compression there is an algorithm computing most general unifier for unifiable formulas.
\end{theorem}

Proof. Given a formula $\varphi(x_1, ... , x_n)$. First we verify if it is unifiable in $L$ at all. For this we
  verify its truth in the one element frame. If for some  valuation $\delta_1$, where  $\delta_1(x_i) := g_i$ ($g_i \in \{\top, \bot\})$, for its letters $x_i$, $\delta_1(\varphi) = \top$ holds then the formula $\varphi(x_1, ... , x_n)$ is unifiable in $L$.   If
  for all possible  $g_i$ it is not the case then formula $\varphi$  is not unifiable in $L$.
  We assume that $\varphi(x_1, ... , x_n)$ is unifiable  in $L$, fix $g_i$ and continue.
  So, we take and fix a substitution   $\sigma_1(x_i) := g_i$ where
 $\varphi(\sigma_1(x_i), \dots, \sigma_1(x_n)) \in L$, if no  such $g_i$, we chose and fix $g_i$ to be those which make false
 $\varphi$ at the one-element model after substitution $g_i$ in place of $x_i$.


Now for
any letter $x_i$ occurring in $\varphi$ we define the following substitution:

\[\sigma(x_i) := \left([\Box^+\Box^-]^{k+1} \varphi(x_1, ... , x_n) \wedge x_i \right) \ \vee
[\neg  [(\Box^+\Box^-)^{k+1} \varphi(x_1, ... , x_n)] \wedge  g_i]. \]


\begin{lemma}\label{lmn4}
$\sigma(x_i)$ is a unifier for  $\varphi$.
\end{lemma}

Proof. By our assumption the logic $L$ is generated by a set $G$ of closed models $M_m$ and these models has
$k$-zig-zag compression property.
  Take a model $M_m$ of this sort. Take and fix a state $x$ from $M_m$.  Only two cases are  possible:

\smallskip

(I) $(M_m,x) \nVdash_V  [\Box^+\Box^-]^{k+1} \varphi(x_1, ... , x_n)$, or



 (II) $(M_m,x) \Vdash_V  [\Box^+\Box^-]^{k+1} \varphi(x_1, ... , x_n)$.

 Now it remains to show that the formula $\sigma(\varphi)$  is true at each $x$ from  $M_m$.

 \medskip


\begin{lemma}\label{lmn4hss}  If (II) it a case then
$\sigma(\varphi)$ is true at all states of $M_m$.
\end{lemma}

 Indeed, consider any state $y$ from
 $M_m$. We know that $x$ is a state of $M_m$, and since the model $M_m$ is closed, there is
zig-zag path P from $x$ to $y$.
Because by condition of this theorem, the frame of the model $M_m$ has
 $k$-zig-zag compression, there is a path
 P from $x$  to $y$ with length
 at most $k$.

  Then by  \[(M_m,x) \Vdash_V  [\Box^+\Box^-]^{k+1} \varphi(x_1, ... , x_n)\]
   we obtain $(M_m,y) \Vdash_V \varphi(x_1, ... , x_n)$.
   Because this holds for any $y$ from $M_m$,
  We get
  \[ (M_m,y) \Vdash_V [\Box^+\Box^-]^{k+1} \varphi(x_1, ... , x_n).\]
  Therefore
  $(M_m,y) \Vdash_V \sigma(x_i)$ for all $y$ from $M_m$. That is because the truth value of any $x_i$ at any $y$
  w.r.t. the original valuation $V$ is exactly the same as the truth value of $\sigma(x_i)$ w.r.t. $V$.
  Because $(M_m,y) \Vdash_V \varphi(x_1, ... , x_n)$ we get $(M_m,y) \Vdash_V \sigma(\varphi(x_1, ... , x_n)).$
  It concludes the proof of this lemma.

  \bigskip


\begin{lemma}\label{kn4hss}  If (I) holds  then
$\sigma(\varphi)$ is true at all states of $M_m$.
\end{lemma}

  Let
\[(M_m,x) \Vdash_V \neg [\Box^+\Box^-]^{k+1} \varphi(x_1, ... , x_n).\]
Then there is a zig-zag path from $x$ to some $y$ from $M_m$ where
\[(M_m,y) \Vdash_V \neg \varphi(x_1, ... , x_n).\]

Since the model is closed, we have that  for any $z$ from $M_m$ there is a zig-zag path
from $z$ to $y$.
By  $k$-zig-zag compression property, there is a zig-zag path
from $z$ to $y$ of length at most $k$.
 So at any $z$



\[(M_m,z) \Vdash_V \neg [\Box^+\Box^-]^{k+1} \varphi(x_1, ... , x_n).\]
So we get that for any $z$ from $M_m$, the truth value of
  any  $\sigma(x_i)$  at $z$ is $g_i$.
  By choice of $g_i$   we get $(M_m,z) \Vdash_V \sigma(\varphi(x_1, ... , x_n)).$
  Lemma is proved.

\bigskip


\begin{definition}\label{ty}
 A set of unifiers $CU$ for a given formula $\varphi$ in a logic $L$ is a complete set of
unifiers, if the following holds. For any unifier
$\sigma_1$ for $\varphi$ in $L$, there is a unifier $\sigma$ from $CU$, where $\sigma$ is more general than
$\sigma_1$, that is there is a substitution $\sigma_2$ such that for any letter $x_i$, $\sigma_1(x_i) = \sigma_2 (\sigma(x_i))$.
\end{definition}



\begin{definition}\label{ty1} We tell that a formula $ \varphi $ is almost-projective (denotation -- alpr) in our logic $L$
if the following holds. There is a substitution $\sigma$  (we call it alpr-substitution) which is an unifier for $\varphi$ and


 \[   [\Box^+\Box^-]^{k+1} \varphi \ii [ x_i \equiv \sigma (x_i)] \in L\]
  for any letter $x_i$ from $\varphi$.
\end{definition}

We see that our definition here is depending on the number $k$, which is fixed during definition of our logic.

\begin{lemma} \label{ty7} If a substitution $\sigma_p$ is alpr for
a formula $\varphi$  in our logic $L$, then $\{  \sigma_p   \}$ is a complete set of unifiers
  for $ \varphi$ (i.e. $\sigma_p $ is most general unifier).
\end{lemma}

 Indeed,
Since we assume that $\sigma_p$ is alpr for $\varphi$ in $L$, we have
$ [\Box^+\Box^-]^{k+1} \varphi  \ii [x_i \equiv \sigma_p(x_i)] \in L$ for any letter $x_i$ from $\varphi$. Take an arbitrary unifier $\sigma_2$ for $\varphi$. Acting by $\sigma_2$ on the formula above we get
\[ \sigma_2( [\Box^+\Box^-]^{k+1} \varphi) \ii [\sigma_2(x_i) \equiv \sigma_2 (\sigma_p (x_i))] \in L.\]


Since $\sigma_2$ is a unifier for $\varphi$, we have $ \sigma_2(\varphi)   \in L $    and $[\Box^+\Box^-]^{k+1} \sigma_2(\varphi) \in L  $.
Therefore
 $\sigma_2(x_i) \equiv \sigma_2 (\sigma_p (x_i)) \in L $. Q.E.D.

\medskip


\begin{lemma}\label{lmn4e}
$\sigma(x_i)$ is an alpr for  $\varphi$.
\end{lemma}


Proof. We shown already that $\sigma$ is a unifier for $\varphi$, and it remains to show that

\[   [\Box^+\Box^-]^{k+1} \varphi \ii [ x_i \equiv \sigma (x_i)] \in L\]

 Take a closed model $M_m$ with $k$-zig-zag compression.
 Take   any state $y$ from
 $M_m$. $\sigma$ is, as we proved above, a unifier for $\varphi$ and hence $\sigma(\varphi)$ is true in any state of $M_m$.
 Therefore $(M_m,y) \Vdash_V \sigma(\varphi)$ for any $y$ and for any $y$,
 $(M_m,y) \Vdash_V [\Box^+\Box^-]^{k+1} \sigma(\varphi)$.
 Hence by definition of $\sigma(x_i)$ above
  the truth value of any $x_i$ at any $y$
  w.r.t. the original valuation $V$ is exactly the same as the truth value of $\sigma(x_i)$ w.r.t. $V$.
 Q.E.D.

 \medskip



\begin{theorem}  Admissibility problem for logic $L$ is decidable.
\end{theorem}

Proof. Indeed, for any rule  $\varphi_1, \dots \varphi_n /  \psi$
 we may compute if it is admissible in $L$ as follows.
An inference rule $\varphi_1, \dots \varphi_n /  \psi$ is not admissible in $L$ iff there is a unifier $\sigma_1$ for
 $\varphi_1 \wedge  \dots \wedge \varphi_n$ which is not a unifier for  $\psi $. But if so,  then the computed by us above   unifier  $\sigma_p$ for $\varphi_1, \dots \varphi_n$ (cf. Lemmas \ref{lmn4}, \ref{ty7}, \ref{lmn4e})    does the same for $\varphi_1, \dots \varphi_n$ and $\psi $ as $\sigma_1$ above.
  $Q. E. D.$



\begin{thebibliography}{190}






\bibitem{kb3}
 Baader F., Snyder W. {\em  Unification theory.} In: Robinson J. A., Voronkov A., editors. Handbook of Automated Reasoning. I. Elsevier Science Publishers
(2001), 447 -- 533.




\bibitem{bg4}
 Baader F., Ghilardi S. {\em
Unification in modal and description logics.}
Logic Journal of  IGPL,  19 (6) (2011), 705 -- 730.




\bibitem{ba21}
Balbiani Ph., Mojtahedi M.
Unification with parameters in the implication fragment of classical propositional logic. {\it Log. J. IGPL},  30(3): (2022), 454-464.

 \bibitem{ba22}         Balbiani, Ph.
Unification in modal
logic.
(2019) In: Indian Conference on Logic and Its Applications
(ICLA), 1 March 2019, -
5 March 2019 (Delhi, India),
DOI : $https://doi.org/10.1007/978-3-662-58771-3_1$.



\bibitem{bs23}
  Bashmakov S., Kosheleva A., Rybakov V.
Non-unifiability in linear temporal logic of knowledge with multi-agent relations.
Siberian Mathematical Reports,
 13 (0), 2016,  656-663.




\bibitem{dw36}
  Dzik W., Wojtylak P. {\em Projective unification in modal logic.} Logic Journal of IGPL 20 (1) (2012), 121 -- 153.



\bibitem{g11}
Ghilardi S. {\em Unification Through Projectivity.} J. of Logic and Computation, 7(6) (1997),
733 -- 752.




 \bibitem{g13}  Ghilardi S. {\em Unification in Intuitionistic logic. } - { Journal
of Symbolic Logic},  64 (2):859-880 (1999)




 \bibitem{g14} Ghilardi S.
{\em Best solving modal equations.}
 { Annals of Pure and Applied
Logic,} 102  (2000), 183 -- 198.




\bibitem{ga24}
 Gabbay D.M., Hodkinson I.M. and Reynolds M.A.
  {\em Temporal
Logic:} - { Mathematical Foundations and Computational Aspects,}
V. 1. Clarendon Press, Oxford, 1994.

\bibitem{ga25}
  Gabbay D.M., Hodkinson I.M.
 {\em An axiomatisation of
the temporal logic with Until and Since over the real numbers.} -
{Journal of Logic and Computation}, 1 (1990),  229 -- 260.



\bibitem{ie19f}
 Iemhof R. {\em On the admissible rules of intuitionistic propositional logic.}
 Journal of Symbolic Logic 66 (2001), 281 -- 294.



 \bibitem{ie20f}
Iemhoff R., Metcalfe G. {\em Proof theory for admissible rules.}
 Annals of Pure and Applied Logic, 159 (2009),  171 -- 186.


\bibitem{je16}
Jer\'abek E. {\em Admissible rules of modal logics.} Journal of Logic and Computation, 15 (2005), 411 -- 431.



\bibitem{je17}
Jer\'abek E. {\em Independent bases of admissible rules.} Logic Journal of the IGPL, 16 (2008), 249 -- 267.




\bibitem{kb2}
   Knut D,,  Bendix  J. Leech G., ed. {\em Simple Word Problems in Universal Algebras.} Pergamon Press. (1970), 263 -– 297.

\medskip



\bibitem{rob1}
  Robinson A. {\em A machine oriented logic based on the resolution
principle.} J. of the ACM, 12(1) (1965),  23 -– 41.


\bibitem{r8}
 Rybakov V.V. {\em
 Problems of Substitution and Admissibility in the Modal System Grz and in Intuitionistic Propositional Calculus.}
 Annals of Pure and Applied Logic, 50(1), (1990)  71 -- 106.



\bibitem{r9}
 Rybakov V.V. {\em  Rules of Inference with Parameters for Intuitionistic
logic.}-  J. of Symbolic Logic, 57 (3) (1992),  912 -- 923.


\bibitem{r10}
  Rybakov V.V.  {\em Admissible Logical Inference Rules.}
{ Series:  Studies in Logic and the Foundations of Mathematics,
Vol. 136, Elsevier Sci. Publ.,}  North-Holland, 1997.





% \bibitem{ga26}    [26]
 %Gabbay D.,  Hodkinson I,. {\em Temporal Logic in Context of Databases.} In J. Copeland, editor, Logic and Reality, Essays on the legacy %of Arthur Prior, Oxford University Press, 1995.




%  \bibitem{ma27} [27]
%Manna Z., Pnueli A. {\em The Temporal Logic of Reactive and Concurrent Systems: Specification.} Springer (1992).



 % \bibitem{ma28}   [28] Manna Z., Pnueli A. {\em Temporal Verification of Reactive Systems: Safety.} Springer (1995).


%\bibitem{vs29}
% [29]
%Vardi M. Y. {\em Reasoning about the past with two-way automata.} In: Larsen K.G., Skyum S., Winskel G., editors. ICALP, LNCS, Springer, %1443 (1998),
%628 -- 641.




\bibitem{va30}
  Rybakov V. V. {\em Linear temporal logic with until and next, logical consecutions}. Annals of Pure and Applied Logic, 155 (2008),
32 -- 45.

\bibitem{br31}
Babenyshev S., Rybakov V. {\em Linear temporal logic LTL: basis for admissible rules.} Journal of Logic and Computation 21 (2011),  157 -- 177.


\bibitem{r32}
 Rybakov V.V. { \em Logical Consecutions in Discrete Linear Temporal
Logic.}  J. of Symbolic Logic,  70 (4) (2005),  1137 --
1149.

%\bibitem{r33}
 %[33] Rybakov V. {\em
%Logics with Universal Modality and Admissible Consecutions.} -{
%Journal of Applied Non-Classical Logics},  17 (3) (2007),
%381 -- 394.

\bibitem{r34}
  Rybakov Vladimir V. {\em  Writing out Unifiers in Linear Temporal Logic.}
 J. Logic Computation, 22 (5) (2012), 1199 -- 1206.



%\bibitem{r35}
%[35] Rybakov V. {\em Unifiers in transitive modal logics for formulas with coefficients (meta-variables) Logic Journal of  IGPL } 21(2) %(2013), 205 -- 215.





\bibitem{wr37}
 Wr\'onski A. {\em Transparent Unification Problem}, Reports on Mathematical Logic 29 (1995), 105 -–
107.


\bibitem{wr38}
  Wr\'onski A. {\em Transparent Verifiers in Intermediate Logics,} Abstracts of the 54-th Conference in
History of Mathematics, Cracow 2008.



%\bibitem{km39}
% [39]
%Kroger F., Merz S. {\em Temporal Logic and State Systems},
%Texts in Theoretical Computer Science. An EATCS Series. Springer; 2008.





\end{thebibliography}


%\end{thebibliography}

\end{document}



\end{document}




\bigskip
\begin{thebibliography}{1} % Ссылки на литературу приводятся только на английском языке (даже если у источника нет англоязычной версии).


\bibitem{1} D.G. Northcott,
\href{https://doi.org/10.1017/CBO9780511565908}{\it Ideal Theory}, Cambridge University Press, Cambridge, 1953.

\bibitem{2} I.I. Ivanov,
\href{https://doi.org/10.1002/cpa.20282}{\it Some properties of commutative algebras}, Siberian Electronic
Mathematical Reports, {\bf 1} (2004), 142--143.

\bibitem{3} A.V. Tetenov, M. Samuel, D.A. Vauilin,
\href{https://doi.org/10.21538/0134-4889-2017-23-4-281-291}{\it On dendrites generated by polyhedral systems and their ramification points}, Trudy Inst. Mat. Mekh. UrO RAN, \textbf{23}:4 (2017), 281--291.

\end{thebibliography}
\end{document}
