






\documentclass{article}
\usepackage{amssymb,amsmath,latexsym}
\usepackage[utf8]{inputenc}

\usepackage[cp1251]{inputenc}  %% 1
\usepackage[russian]{babel}
\textwidth=140truemm \textheight=225truemm
\oddsidemargin=1.24truecm \evensidemargin=0.46truecm
\voffset-2cm\hoffset-.5cm





\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}
\newtheorem{definition}{Определение}
\newtheorem{corollary}{Corollary}
\newtheorem{proposition}{Proposition}

\title{Мульти-Агентные  Логики с Взаимодействием,  Унифицируемость и Проективность.\\
In English -- Multi-Agent Logics with agents' Interruction,  Unification and Admissibility.
}

\date{}


\author{В.В.Рыбаков, V.V. Rybakov \\
\it Институт Математики и Фундаментальной Информатики,\\
Сибирский Федеральный  Университет, \\
Свободный 79, Красноярск \\
660 041, и  Институт Систем \\ Информатики РАН, Novosibirsk\\
Vladimir\_Rybakov@mail.ru; \\
In English - V.V.Rybakov, Institute of Mathematics and Fundamental Informatics,\\
Siberian Federal University, av. Svobodnui 79, Krasnoyarsk, 660 041 and \\
(pat time) Institute
Systems in Informatics RAN, Novosibirsk, Vladimir\_Rybakov@mail.ru
 }





 \usepackage{latexsym,fleqn}





\begin{document}



\maketitle



УДК 510.64,510.65,510.66

\bigskip

{ \Large \bf  Аннотация}.  \footnote{ Работа поддержана РНС - No.23-21-
00213) - Russian Scientific Foundation (Project No.23-21-
00213) }  {\it
Данная работа изучает много-агентные не классические модальные логики, порождаемые реляционными Крипке--подобными
   моделями, описывающими передачу информации Мы вводим Крипке-подобные модели существенно расширяющие обычные модели Крипке. Исследуются алгоритмические проблемы возникающие в таких логиках. Решается проблема разрешимости для таких логик, находятся алгоритмы, проверяющие выполнимость формул. Решается проблема допустимости в таких логиках на основе техники проективности формул и унификации.



 This paper works with multi-agent none-classical  modal logics generated by relational Kripke-like models describing transfer information and it reliability. We suggest Kripke-lilke Kmmpdels  essebtally extendinf usual multi-model Kripke semantics. We plimarely study algorithmic problems connected with such logics. Our aim is finding the proof that suck logics are decidable, finding algorothms verifyinh stasfiability frmulsd, we solve the problem of adimiibility interence rules via technique of projective formulas and unification, we prove that this problem is decidable   }





\bigskip

 {\large Ключевые слова: } {\sl модальные логики,
 мультиагентные логики, информация, знание,
 проблемы унификации и допустимости,
разрешающие алгоритмы}

%%%%%%%MY Symbols



\newcommand{\llll}{{\cal LT \hspace*{-0.05cm}L}}

\newcommand{\llln}{{\cal LT \hspace*{-0.05cm}L}_{NT}}


\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{\nv}[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}}
\protect{ \put(0.3,-0.7){\line(1,1){3.6}}}
\end{picture}\hspace*{0.3mm}
} }

\newcommand{\nn}{{\bf N}}

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


\newcommand{\uu}{{{\bf U}}}

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

\newcommand{\sss}{{{\bf S}}}


\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{\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{\cff}{{\cal F}or}

\newcommand{\cc}{{\cal C}}
\newcommand{\cf}{{\cal F}}


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


\newcommand{\cw}{{\cal W}}
\newcommand{\cx}{{\cal X}}
\newcommand{\cz}{{\cal {\cal Z}}}
\newcommand{\hc}{{\cal H}}
\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{\cm}{{\cal M}}
\newcommand{\ty}{{\cl_{t,y}(\cz)}}
\newcommand{\cll}{{\cal L}}
\newcommand{\ckk}{{\cal K}}
\newcommand{\cmm}{{\cal M}}
\newcommand{\czz}{{\cal Z}}
\newcommand{\lla}{{\cal LT \hspace*{-0.05cm}L}}
%\newcommand{\llll}{\mathrm{LTL}_{\mathcal{ACK}}}
\newcommand{\ltl}{\mathcal{LTL}}

\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{\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}
} }




\newcommand{\suu}{{{\bf S}}}



\newcommand{\nnn}{{\cal N}}



\begin{document}



\maketitle





\section{\bf Введение}


Многоагентные  и модальные логики активно используюсь в проблематике искусственного интеллекта и информатике начиная с 1980гг. Суммирование полученных к начальному времени результатов исследований можно найти в книге
\cite{faa2}.

Анализируя этот подход, мы ранее предложили его обобщение, используя вместо формулы -- знает $K_i A$ --
общее определение для информируемости агентов.
 Этот подход описан в  Rybakov \cite{rraa2z}, в той работе найдены теоремы о разрешимости таких логик и их приложения. С тех пор было уделено много внимания приложениям много-агентных модальных логик к проблемам построения формальный моделей для концепции знание (см. [2], \cite{ar1, ar2,ar3,ry2}, [6,7, 8--16).

 В этой нашей работе мы исследуем много-агентные не классические модальные логики, порождаемые реляционными Крипке--подобными
   моделями, описывающими доступ агентов к информации и ее передачу.
   Эти модели  существенно
   расширяют стандартную семантику Крипке, в них моделируются различные методы доступа агентов к информации. Основная цель -- исследование алгоритмические проблемы возникающие в таких логиках. Мы находим решение проблемы разрешимости для таких логик, находим алгоритмы, проверяющие выполнимость формул. На основе техники проективности формул и унификации
      решается проблема допустимости правил вывода в таких логиках.
 }




\section{ \bf Мульти-Агентные  Логики с Взаимодействием}

Начнем с модификации, предполагающей введение изолированных групп экспертов с редактируемыми правилами доступа к информации. Итак, основным стартовым объектом является линейный временной фрейм

 \[ \bf  F := \langle \bigcup_{i \in N} C(i), \leq \rangle\]
 где  $\bigcup_{i \in N},  C(i)$ это просто множество -- это множество состояний (миров, временных состояний, $i \in N$ это индексы временный состояний, обозначаемые натуральными числами,  $C(i)$ -- некоторые множества состояний (элементов, миров) доступных в текущий момент времени $i$.) Для
 $a \in C(i_1), b \in C(i_2)$, $a \leq b$ если и только если $i_1 \leq i_2$. То есть $\leq$ это линейное (но не частично упорядоченное) отношение временной достижимости.

 Фиксируется некоторое конечное множество индексов $J$ для агентов,  и для каждого агента $j \in J$ и каждого $C(i)$  фиксируется некоторое подмножество  -  группа
 состояний (миров, элементов) с которые агент   может консультироваться об истинности утверждений.
 Основа предлагаемой нами новой модификации состоит в разделение линейных временных состояний, принятый в предпринятом ранее анализе на собственно временные дискретные состояния (сегодня, завтра, послезавтра) и  последующее разделение линейных временных состояний на доступные в это время информационные состояния (базы данных, веб сайты и пр.) доступные агентам для консультаций.  Этот подход изначально может быть проинтерпретирован следующим образом.

\medskip

  {\bf Определение 1. } Временной многоагентный фрейм это

  \[ \bf  F := \langle \bigcup_{i \in N}  C(i), \leq, R_j, j \in J \rangle\]
 где при $ i \in N$ и любое $C(i)$    является просто некоторым множеством (называемым интерпретируемым как все информационные базы данных (веб узлы), доступные во время $i$). При разных $i_1$  и $i_2$ множества $C(i_1)$ и $C(i_2)$ предполагаются непересекающимися.

\medskip

 Фиксируется некоторое конечное множество агентов $J$; любое $J$ разбито на непересекающиеся множества агентов--экспертов,
$J = J_1 \cup J_1 \cup ... \cup J_k$. Каждому $J_m$ в любом $C(i)$ соответствует некоторое подмножество
$Q(J_{i,m})$ множества $C(i)$ и все $Q(J_{i,m})$ также предполагаются непересекающимися.

Бинарные отношения достижимости агентов $R_j$ между состояниями любого множества $C(i)$ для любого $j \in J$ определяются следующим образом

\[\forall a,b \in C(i), a R_j b \iff \exists Q(J_{i,m}) (a,b \in Q(J_{i,m})).\]

То есть, все агенты из $J_m$ могут видеть все состояния из $Q(J_{i,m})$  (внутри любого $C(i) $) и только эти состояния. Это значит, что они обладают абсолютно равными и одинаковыми возможностями для консультации об истинности информации. Это представляется реалистичным и более точным подходом к согласованию истинности информации.
 А именно, в любой фиксированный момент текущего времени (сегодня, например), для каждого эксперта существует некоторое фиксированное сообщество экспертов с которым эксперт может взаимно обмениваться информацией о том истинно ли утверждение.

Естественно любой фрейм превращается в модель введением означивания логических переменных, а именно

\medskip

  {\bf Определение 2. } {\it Модель на фрейме
  $F$ задается введением некоторого  означивания
 $V$ на $F$  некоторого множества пропозициональных переменных   $p$, где
$V(p) \subseteq   \bigcup_{i \in N}  C(i) $. Все состояния из $V(p)$ трактуются как те на которых переменные $p$  истинны относительно $V$.}

\medskip

Логический язык стандартно включает все булевские логические операции, модальные операции
$\Box$  и $\Diamond$ и унарные логические операции  $K_i$ для всех  $i \in J$,   $K_i \varphi$  - означает -- агент $i$  знает
$\varphi$ или агент $i$  может узнать
$\varphi$   (мы не фиксируем жестко трактовку). Отношения определяющие истинность логических операций перечислены ниже.

\bigskip

{\bf Определение 3.}  $\forall a\in T(M)  $:
\(  \left(F,a\right) \Vdash_{V}  p  \ \Leftrightarrow \ \  p \in V(p);\)

\medskip

для всех булевых операций определения вычисления истинности обычные и }  \\

\medskip

\(\forall a \in C(i)  \ \ [ (F,a) \Vdash_{V} \Box \varphi\  \Leftrightarrow
\ \
\forall b \in C(j) ( i \leq j \Rightarrow (F,b )\Vdash_{V} \varphi ) ) )]; \ \)

\medskip

\(\forall a \in C(i) \ \  [(F,a\right) \Vdash_{V} \Diamond  \varphi\  \Leftrightarrow
\exists b \in C(j) ( i \leq j) \& (F,b)\Vdash_{V} \varphi) ).] \ \)

\medskip

Истинность логических операций знания $K_i$  определяются так:

\[\forall a \in C(i) \ [ (F,a) \Vdash_{V} K_i  \varphi \  \Leftrightarrow
\exists b [ (a R_i b)  \& (F,b)\Vdash_{V} \varphi )]
 \vee
[(F,a)\Vdash_{V} \varphi  ]) ]. \ \]


При такой интерпретации  $K_i  \varphi$ означает, что агент может узнать, хотя бы раз, что
$\varphi$ бывает истинно.


Далее уже стандартным образом, по любому фиксированному классу моделей определяются логики, а  именно

\bigskip


{\bf Определение 4.} \label{d}  {\it Для  класса всех фреймов $K$, определенных выше (для каждого зафиксированного конечного множества агентов $J$), многоагентная логика $LMA(K)$, порожденная  $K$, это множество всех формул истинных а всех состояниях фрейма при всех означиваниях}

\bigskip

{\bf Теорема 5. } {\it  Логика $LMA(K)$ разрешима, существует алгоритм
 проверяющие выполнимость формул.}

 \medskip

 Доказательство.
 Заметим, что прямой метод вариаций фильтраций здесь неприменим потому что если случиться что в отдельном
 C(i) все истинностные значения подформул одинаковые и совпадают с истинностными значениями
 подформул на некоторым состоянии фрейма стоящим отдельно и вне $С(i)$  мы будем вынуждены сливать это внешнее  состояние с некоторым состоянием из $С(j)$ и следовательно пересекать разные компоненты фрейма,
что противоречит выбранному семантическому заданию логики, а также могут возникнуть и другие коллизии. Поэтому необходима предварительная несложная трансформация
техники фильтрации и структур фреймов под рассмотрением, и, затем, последующая техника просеивания моделей.
Итак, допустим, что формула $\ppp$ выполняется в некоторой модели

\[(F,V) := \langle \bigcup_{i \in N}  C(i), \leq, R_j, j \in J, V\rangle\] на некотором состоянии
$a$, $(F,a) \Vdash_V \ppp$;  мы тогда естественно можем предположить, что имеет место $a \in C(0)$.


 Первый шаг доказательства состоит в том, что мы изолируем каждый подсгусток $Q(J_{i,m})$ в любом временном сгустке С(i) и проводим отделано стандартную фильтрацию только внутри этих $Q(J_{i,m})$.
 В нашем данном случае это выглядит так:

 \[ \forall x,y \in Q(J_{i,m})  [ x \equiv_J y \lri [\forall p \in Var(\ppp)[
 x\Vdash_V p \lri  y\Vdash_V p ]].\]
 Понятно что  $\equiv_J $ является отношением эквивалентности, и мы замещаем любой $x \in
 Q(J_{i,m}$ классом эквивалентности $[x]_J$, оставляя между ними все те же отношения достижимости. Эту процедуру мы выполняем с каждым $Q(J_{i,m})$ в любом сгустке $C(i)$. Состояния расположенные вне множеств
 $Q(J_{i,m})$ остаются без изменений.

 Этим способом мы выполняем только эту фильтрацию но, отдельно, на каждом $C(i)$ точно таким же образом как указано выше. Затем выполняем фильтрацию на всех $C(i)$ отдельно но только на состояниях не затронутых предыдущими фильтрациями.
 Этим способом мы выполняем только эту фильтрацию полностью,  но отдельно на каждом $C(i)$. Легко проверить индукцией по длине формул, что указанная трансформация обладает всеми необходимыми свойствами фильтраций, в частности оно сохраняет истинность формул


 \[ \forall x \in F, \forall \psi \in Sub(\ppp)
   [ (F,x) \Vdash_V \psi   \ \  \lri \   \ \ (F_{\equiv_J},[x]_J) \Vdash_V \psi]\]

В итоге каждый сгусток$C(i)$  в полученной модели становится конечным с числом состояний ограниченным числом вычислимым по размерности множества $Sub(\ppp)$. Далее работаем с только такими моделями и выполняем далее технику просеивания.


А именно теперь, рассматриваем все из получившихся в результате этой конструкции модели $C(i)$  внутри всего фрейма как идентичные если они изоморфны. Пусть

\[\forall n \in N, \ M(n) := \{C(i) \mid i\geq m\}.\]
Ввиду того, что осталось только конечное число таких моделей C(i) и их число ограничено
числом вычислимым их числа подформул множества $Sub(\ppp)$, получаем, что существует число
$st \in N$, такое что

\[M(st) = M(k), \forall k \geq st. \]
Пусть

\[ Repr(st) := \{C(i_1, \dots , C(i_t)   \} \]
это множество всех возможный различных моделей такого сорта из $M(st)$ при $i_j > st$.
Порядок и последовательность выбора представителей неважных, но индексы $i_j$ взяты в возрастающем порядке. Далее выберем множество

\[ Repr(st2) := \{C(k_1, \dots , C(k_t)   \} \]
которое тоже является множество всех возможный различных моделей $C(i)$ но уже из $M(i_t)$ при $k_j > i_t$.
(снова порядок и последовательность выбора представителей неважны, но индексы $k_j$ взяты в возрастающем порядке).   Теперь преобразуем получившуюся модель, считая временной индекс следующим за $k_t$ число $st$ и удаляя полностью все сгустки выше времени $k_t$.
Обозначим получившуюся модель через $M_1$.


\bigskip

{\bf Лемма 6. }
Для любой формулы $\psi$ из $Sub(\ppp)$ и для любого $ a \in M_1$

\[(M_1,a) \Vdash_V \psi    \iff (M,a) (M,a) \Vdash_V \psi.    \]

\medskip


Доказательство следует несложной прямой индукцией по длине формул $\psi$ учитывая выбор чисел $st$ и $k_t$ выше и выбор всех оставшихся в модели сгустков $C(i)$. $\Box$

\medskip

Если же выполняется $(M_1,a) \Vdash_V \ppp$ для некоторой такой конечной модели
$(M_1)$,  то разворачивая цикл сгустков расположенных между $C(st)$  и  $C(k_t)$ в возрастающую бесконечную цепь, получаем что $(M,a) \Vdash_V \ppp$ и для некоторой стандартной бесконечной модели
$M$.

Таким образом, благодаря этой лемме, мы сводим вопрос о выполнимости в логике $LMA(K)$,   порожденной бесконечными моделями с произвольной структурой моделей, к выполнимости формул на конечных моделях вида
$M_1$ размера не выше вычислимого по размеру формулы.
Теорема доказана. $\Box$.

\bigskip


Рассмотрим  возможный вариант определения локального знания, локальной информации агентов, через предложенные семантические модели.
 Один из возможных путей выглядит так (итак пусть логическая связка $LCK$ интерпретируется как обозначение для локального знания).




\[\forall {\bf a \in C(i)  \ \ [\left(F,a\right) \Vdash_{V} LCK } \varphi\  \Leftrightarrow
[(F,a\right)\Vdash_{V} \varphi] \vee \]
\[[ \exists j \in J$,
\exists b \in C(i) ( a R_j b \ \& \ (F,b)\Vdash_{V} \varphi \right) ] ].\ \]
Ясно что эта связка очевидно выразима в предложенном логическом языке, а именно

\[ LCK  \varphi \ \ \equiv  \ \varphi \ \vee \bigvee_{j\in J} K_j \varphi.\]

То есть это означает что  либо формула $\varphi$ истинна уже в текущем состоянии (на $a$) любо существует агентные отношение достижимости
из $a$ к состоянию  - базе данных -- которая знает $\varphi$.
Локальность здесь означает, что  это возможно только внутри текущего кластера времени.
 $C(i)$.
  Думается, что такой подход разумен и хорошо совпадает часто с реальной регламентацией работы агентов для получения информации.

\medskip

Сейчас мы введем еще один возможный способ формализовать локальное общее знание.
Идея состоит в том чтобы не назначать никакой регулярной системы изолированных баз знаний для только экспертов, а регламентировать доступ к информации предписанием агентам администратором.
 В принципе принятый подход состоит в том, что любому агенту жестко назначено множество состояний и агентов с которыми он может консультироваться и получать от них информацию.
 Формально это выглядит следующим образом.

\bigskip

  {\bf Определение 7. } Фрейм внешне выглядит как и в предыдущем определении

  \[ F := \langle \bigcup_{i \in N} C(i),
\leq, R_j, j \in J \rangle.\]
 И любое $R_j$ это просто бинарное отношение на любом $C(i)$ и $R_j$ не является отношением эквивалентности и даже не  транзитивно. Задается оно следующим образом. Выбирается некоторое зафиксированное множество состояний $a \in C(i))$ и для каждого из них зафиксировано некоторое множество состояний $In_a \subseteq C(I)$ с которыми агент $j$ может консультироваться находясь в состоянии  $a$:

 \[ R_{j,a}  := \bigcup  \{ <a,b> \mid b \in In_a\} \cup \{<a,a>\}. \]

То есть теперь поведение  $R_{j,a}$ не регулярно и полностью определено так сказать администратором (хотя думается это хорошо соответствует решениям принятым реальным администраторам). Помимо этого, мы предполагаем что различные множества
$R_{j,a}$  полностью не пресекаются - не имеют общих состояний вообще. Это сделано для того чтобы избежать возможных коллизий при попытках модифицировать технику фильтрации.

Для моделей на таких фреймах мы таким же как и ранее образом определяем вычисление истинности логических операций, в частности $K_j$. Как и ранее логика вводится обычным образом.

\medskip



{\bf Определение 8.} \label{d}  {\it Для  класса  $K$ указанных фреймов, многоагентная логика $LRI$ порожденная  $K$ это множество всех формул истинных а всех состояниях таких фреймов при всех возможных означиваниях.}

\bigskip

{\bf Теорема 9.  } {\it  Логика $LRI$ разрешима, существует алгоритм,
 проверяющий выполнимость формул.}

 \medskip

 Доказательство. Мы вначале изолируем каждое множество

  \[ R_{j,a}  := \bigcup  \{ <a,b> \mid b \in In_a\} \cup \{<a,a>\}\]
   и выполняем на нем следующие преобразования.  Пусть


 \[ \forall x,y \in In_a  [ x E_J y \lri [\forall p \in Var(\ppp)[
 x\Vdash_V p \lri  y\Vdash_V p ]].\]
  Очевидно что это отношение  $E_J$ является отношением эквивалентности на
  $In_a$ и мы берем фактор множество на $In_a$  по $E_J$  и заменяем все $b \in In_a$    там на содержащие их фактор множества. В полученной модели $M_1$ очевидно выполняется


 \[ \forall x \in F, \forall \psi \in Sub(\ppp)
   [ (F,x) \Vdash_V \psi   \ \  \lri \   \ \ (M_1,x_J) \Vdash_V \psi],\]
где $x_J$  это состояние соответствующее $x$ после сделанного преобразования.
Выполним такое преобразование для всех \( R_{j,a} \).

После этого в любом сгустке $C(i)$  получившейся модели из множества всех получившихся
\( R_{j,a} \), изоморфных как модели, удалим все копии оставив только одну такую уникальную модель \( R_{j,a} \).
В полученной таким образом модели $M_2$ очевидно тоже выполняется


 \[ \forall x \in M_1, \forall \psi \in Sub(\ppp)
   [ (M_1,x) \Vdash_V \psi   \ \  \lri \ ]  \ \ (M_2,x_J) \Vdash_V \psi],\]
где $x_J$  это состояние соответствующее $x$ после сделанного преобразования.


Заметим, что после этого преобразования все состояния расположенные вне  \( R_{j,a} \)
остались нетронутыми. Теперь мы выполняем стандартную фильтрацию только на таких состояниях нетронутых предыдущими преобразованиями, но только внутри каждого  $C(i)$
 отдельно.

 В результате получаем модель  $M_3$. Ясно что (это факт легко проверить индукцией по длине формул) эти преобразования сохраняют истинность формул и

 \[ \forall x \in M_2, \forall \psi \in Sub(\ppp)
   [ (M_2,x) \Vdash_V \psi   \ \  \lri \  \ \ (M_3, x_J) \Vdash_V \psi]\]

 После этого получаем, что любое $C(i)$ конечно и имеет число элементов не выше числа эффективно вычислимого по числу подформул формулы $\ppp$.

 Теперь, рассматриваем все из получившихся в результате этой конструкции модели $C(i)$  внутри всего фрейма как идентичные если они изоморфны. Пусть
\(\forall n \in N, \ M(n) := \{C(i) \mid i\geq m\}.\)
После этого  осталось только конечное число таких моделей C(i).

Ясно что  их число ограничено
числом вычислимым из числа подформул нашей формулы $\ррр$. Поэтому получаем, что существует число
$st \in N$, такое что
\(M(st) = M(k), \forall k \geq st. \)
Пусть как и ранее
\( Repr(st) := \{C(i_1, \dots , C(i_t)   \} \)
это множество всех возможный различных моделей такого сорта из $M(st)$ при $i_j > st$.
Порядок и последовательность выбора представителей неважны, но индексы $i_j$ взяты в возрастающем порядке.
Далее мы снова выберем множество
\( Repr(st_F) := \{C(k_1, \dots , C(k_t)   \} \)
которое тоже является множеством всех возможный различных моделей $C(i)$ но уже из $M(i_t)$ при $k_j > i_t$. (снова порядок и последовательность выбора представителей неважны, но индексы $k_j$ взяты в возрастающем порядке).

Теперь преобразуем получившуюся модель, считая временным индексом следующим за $k_t$ число $st$ и удаляя полностью все сгустки выше времени $k_t$.
Обозначим получившуюся модель через $M_4$.

\bigskip

{\bf Лемма 10.}
 Для любой формулы $\psi$ из $Sub(\ppp)$ и для любого $ a \in M_4$

\[(M_4,a)\Vdash_V \psi    \iff (M_3,a) \Vdash_V \psi.    \]

\medskip

Доказательство следует несложной прямой индукцией по длине формул $\psi$ учитывая выбор чисел $st$ и $k_t$ выше и выбор всех оставшихся в модели сгустков $C(i)$. $\Box$

\medskip

В случае когда  выполняется $(M_4,a) \Vdash_V \ppp$ для некоторой такой конечной модели
$(M_4)$,  то разворачивая цикл сгустков расположенных между $(C_{st})$  и  $(C_{k_t})$ в возрастающую бесконечную цепь, получаем что $(M,a)\Vdash_V \ppp$ и для некоторой стандартной бесконечной модели
$M$.

Таким образом, благодаря этой лемме, мы сводим вопрос о выполнимости в логике $LRI$,   порожденной бесконечными моделями с произвольной структурой моделей, к выполнимости формул на конечных моделях вида
$M_4$ размера не выше вычислимого по размеру формулы.
Теорема доказана. $\Box$

\bigskip





\section{\bf Вводная информация по унифицируемости}


Кратко наполним,что подстановка для множества пропозициональных переменных (или букв) $P$
  это некоторое отображение  $\varepsilon$  множества $P$ во множество всех формул
$For$. Любая такая подстановка может быть расширена на множество всех формул с посредством
 $\varepsilon
(\ppp(x_1, \dots , x_n)) := \ppp(\varepsilon(x_1), \dots ,
\varepsilon(x_n))$.



\bigskip

{\bf Определение 11.}
Формула $\ppp$ называется унифицируемой в логике $L$ если существует подстановка
$\varepsilon$ (называемая унификатором формулы $\ppp$) такая что $
\varepsilon(\ppp) \in L$.

%Now we recall the basic definition of our paper:

\medskip

{\bf Определение 12.} {\it
Унификатор $\varepsilon$ для формулы  $\ppp$ в логике $L$ является более общим чем унификатор  $\varepsilon_1$  если существует подстановка
$\delta$ такая что для любой буквы $x$, $[\varepsilon_1(x) \equiv
\delta(\varepsilon(x))] \in L$. }

\medskip



%\begin{definition} \label{lu1} {\em
%A substitution $ \varepsilon$ is a unifier for a formula $\ppp$ in $\llll$ if
%$\varepsilon(\ppp) \in \llll$.  A formula $\ppp$ is unifiable in
%$\llll$ if it has a unifier. A unifier $\varepsilon$ is more general
%than a unifier $\varepsilon_1$ iff there is a substitution $\delta$
%such that for any letter $x$, $\varepsilon_1(x) = \delta(\varepsilon
%(x))$.}
%\end{definition}


%Since the logic $\llll$ is decidable, to check unifiability a formula
%in $\llll$, is the reasonably easy task: it is sufficient to use only
%ground substitutions: mappings of variables in the set $\{\bot,
%\top\}$.

Если логика разрешима, то обычно проверить унифицируемость формул довольно просто
(теоретически, но сложность и длина вычислений может быть недопустимо высокой)
: достаточно использовать только подстановки переменных  в --
истина-ложна --$\{\bot, \top\}$. Но проблема нахождения всех унификаторов
гораздо более сложна.


\medskip

{\bf Определение 13.}
 Множество унификаторов
 $CU$ для данной формулы  $\ppp$ в логике $L$ является полным множеством унификаторов,
 если выполняется следующее. Для любого унификатора
$\sigma$ формулы $\ppp$ в $L$, существует унификатор $\sigma_1$ из $CU$, такой что $\sigma_1$ более общий чем
$\sigma$.


Для модальных логик, расширяющих модальную систему
$S4$  определение проективности формул может быть дано следующим образом.



\medskip

{\bf Определение 14.}
 Формула $\ppp$ называется проективной в логике
 $L$ если выполняется следующее. Существует подстановка
 $\sigma$ (называемая проективной подстановкой для
 $\ppp$) такая что $\sigma$  является унификатором для \ppp$  в   $L$    и  $\Box \ppp \ii [ x_i \equiv \sigma (x_i)] \in L$ for для любой переменной  $x_i$ из $\ppp$.




\medskip

{\bf Лемма 15.}
 Если подстановка $\sigma_p$ проективна для
   $\ppp$  в логике  $L$, то $\{\sigma_p\}$ является полным множеством унификаторов для  $\ppp$ (т.е. подстановка $\sigma_p $ является
   наиболее общим унификатором ).

\medskip

Доказательство. Действительно, пусть  $\sigma$ является унификатором для $\ppp$ в $L$.
Так как  $\sigma_p$ проективна для  $\ppp$ в $L$, мы получаем
$\Box \ppp \ii [x_i \equiv \sigma_p(x_i)] \in L$ для любой переменной  $x_i$ из $\ppp$. Применяя $\sigma$ к формулам выше, мы получаем
$\sigma(\Box \ppp) \ii [\sigma(x_i) \equiv \sigma (\sigma_p (x_i))] \in L $,
то есть $\sigma(x_i) \equiv \sigma (\sigma_p (x_i)) \in L $. Q.E.D.

\medskip

Конечно не все унифицируемые формулы проективны в неклассических логиках, примеры широко известны.


\medskip

Легко видеть, что если для разрешимой модальной логики
$L$, расширяющей $S4$ мы можем определить проективна ли формула $\ppp$ и вычислить ее проективный унификатор, то проблема допустимости правил вывода в
 $L$ разрешима. Действительно, правило вывода
 $\ppp_1, \dots \ppp_n /  \psi$ не допустимо в  $L$  если и только если
 существует унификатор для
 $\ppp_1 \wedge  \dots \wedge \ppp_n$ который не является унификатором для
   $\psi $. Но  тогда вычислимый  более общий унификатор
   получаемый по проективной подстановке для
  $\ppp_1 \wedge  \dots \wedge \ppp_n$
 проверяет это. Эта интересная идея была введена в обиход логиков, работающих
в неклассической логике, Silvio Ghilardi (см. \cite{g1}). Мы применим в этой статье технику проективности для решения проблемы допустимости в изучаемых в этой статье логиках.

\medskip

\section{Разрешимость Допустимости через Проективность}


Применение проективности в данном конкретном случае логик близких к линейным, позволит дать нам очень короткое и компактное доказательство решения проблемы допустимости правил вывода. Такой подход через технику проективности был найден Сильвио Гиларди и впоследствии был применен к линейным модальным логикам
 (Wojciech Dzik, Piotr Wojtylak) для модальных логик, расширяющих S.4.3 [20],  [18,19]
 и затем был развит для временных логик в
 V. Rybakov [17].
 В этом параграфе нам необходима некая легкая модификация многоагентных фреймов, для того чтобы мы могли использовать технику проективных формул.

\medskip

  {\bf Определение 16. } Как и ранее, в качестве фрейма мы можем использовать  любую версию определенную ранее ---

  \[ \bf  F := \langle \bigcup_{i \in N}  C(i), \leq, R_j, j \in J \rangle.\]


\medskip

Но для унификации через проективность нам необходимо присутствие некоторого состояния в каждом кластере  $C(i)$: мы допускаем, что для любого
     $ C(i)$ существует по крайней мере единственное состояние $ Dis \in C(i)$ такое что,

    \[  \forall  i \in N, \forall j \in J, \forall b \in C(i), \
      \ [Dis R_j b   \iff  b = Dis] \ \& \
    [b R_j Dis   \iff  b = Dis]. \]

Этот элемент $Dis$ называем от-соединенным или выключенным (disjoint) так как любой агент не может его достичь по $R_j$  и снять с него информацию, и также будучи в любом другом состоянии не видит по $R_j$ этот элемент (он как бы невидим агентам). В частности, мы полагаем, что в любой модели при любом выбранном означивании на таком фрейме все переменные на элементах типа $Dis$ ложны ( $(M,Dis)\Vdash_V \neg p_j$). Эти ограничения, тем самым, никак не ограничивают выразимость информации но технически полезны для применения проективности. Как и ранее логика   $L$ это множество всех формул истинных на всех таких возможных моделях.


\bigskip

 {\bf Теорема 17.} { \it В логике $L$ любая унифицируемая формула является проективной.
 Унифицируемость формул в этой логике алгоритмически распознаваема. Существует алгоритм, строящий проективный унификатор для любой унифицируемой формулы. Поэтому проблема допустимости правил вывода разрешима для $L$.
}

\bigskip

 Доказательство. Вначале нужно доказать алгоритмическую распознаваемость унифицирумых формул. Эта задача не так тривиальна как для  просто булевой пропозициональной логики, но сравнительно достаточно несложна.  Действительно, пусть дана произвольная формула
  $\varphi(x_1, ... , x_n)$ и она унифицируема. Наша логика обладает в частности моделями  $M$ где каждый кластер $C(i)$
  состоит только из одного состояния Dis.

   Допустим что формула  $\varphi(x_1, ... , x_n)$ унифицируема в логике $L$ и $\sigma_1$ ее унификатор. Пусть подстановка $\sigma_1$  действует следующим образом,

  \[ \forall x_i, \sigma_1( x_i ):= \alpha_i,\mbox{  где }  \alpha_i \in For\]

   При этой подстановке формула $\varphi(x_1, ... , x_n)$ истинна на $M$ так как $\sigma_1$ ее унификатор.
      Тогда истинность любых переменных $y_j$ из формул в указанных формулах $\alpha_i$, участвующих в подстановке $\sigma_1$,  принимают истинностное значение ложь на любом состоянии $Dis$ из этой модели $M$, -- поэтому мы можем считать, что

  \[\sigma_1( y_j) = \bot\]
   и при этой подстановке $\sigma_1$ на этой модели истинна наша формула.  При этом мы не утверждаем, что модифицированная подстановка унификатор в логике, но тем не менее очевидно верна


\medskip

{\bf Лемма 18.}
Для данной модифицированной подстановке \sigma_1

  \[ \forall a \in M, (M,a) \Vdash_V \neg  \sigma_1( y_j).\]


   В этом случае любая из формул $\alpha_i$ при этой подстановке $\sigma_1$ принимает одно и то же истинностное значение истина или ложна одновременно на всех состояниях   из этой модели $М$  (а она состоит только из таких состояний $Dis$).  Поэтому (легкая индукция по длине формул $\alpha_i$) верна



\medskip

{\bf Лемма 19.}
 В модели $M$,
  \[ \forall a,b \in M, \  \forall \alpha_i,  (M,a)\Vdash_V \sigma_1(\alpha_i)  \ \lri \(M,b) \Vdash_V \sigma_1(\alpha_i). \]

  \medskip

  Потому подстановка $\sigma_1$ вместо переменных формулы $\varphi(x_1, ... , x_n)$ просто истинностных значений формул $\alpha_i$ в указанной модели $M$ при том заданном означивании $\sigma_1$,
  будет унификатором формулы $\varphi(x_1, ... , x_n)$ в нашей логике (так как $\varphi(x_1, ... , x_n)$ при  $\sigma_1$   истинна на исходной модели $M$). Поэтому и здесь для проверке унифицируемости достаточно рассмотреть просто одноэлементную модель и истинность на ней.

  Конечно мы не знаем точного значения действия $\sigma_1$ на одноэлементной модели
  (как и в булевой логике), но его можно уточнить простым перебором пользуясь разрешимостью логики (она доказывается как и ранее в этой статье для упомянутых логик, просто в начале доказательства надо слить все состояния типа $Dis$  в любом кластере C(i) в одно состояние). Таким образом проблема распознавания унифицируемости  в таких логиках разрешима.
  Зафиксируем необходимый нам в будущем некоторый вычисленный таким образом унификатор $\sigma_3$ для формулы $\varphi(x_1, ... , x_n)$,

  \[ \sigma_3(x_i) = \delta_i, \mbox{где}  \ \delta_i \in \{\bot,\top\}. \]
  Но вот проблема нахождения наиболее общих унификаторов совсем не так проста.




Приступая к доказательству проективности унифицирумых формул, для любой пропозициональной переменной
 $x_i$ из  любой данной формулы $\varphi$ мы определим следующую подстановку.  Пусть $Var(\Box \varphi)$ является множеством всех пропозициональных переменных из $\Box \varphi$ и
  $Sub(\Box \varphi)$ является множеством всех подформул формулы $\Box \varphi$. Возьмем любое  $X \subseteq Sub(\Box \varphi)$,  и далее фиксируем формулы


%If $X\subseteq $Var(\Box \varphi)$,
%$$
%Let(X) := \bigwedge_{x_i \in Var(\Box \varphi \cap X} x_i \wedge
%\bigwedge_{x_i \in Var(\varphi) \& x_i \notin X} \neg x_i. $$





Пусть для любой переменной $x_i$ из $Var(\ppp)$,


\[\sigma(x_i) := (\Box \varphi)\wedge x_i ]  \vee
[\neg \Diamond \Box  \varphi  \wedge \sigma_3(x_i)]  \vee \]
\[ [\neg \Box \varphi \wedge \Diamond \Box  \varphi \wedge \bot].\]
%\[ \bigwee_{} \Box \neg \varphi_i \ii \Diamond \Box \varphi_i \wedge\]


Докажем, что эта подстановка является унификатором для формулы $\varphi$ в логике $L$.
Выбираем любую модель нашей логики, т.е. любой фрейм
$F$ (с состояниями Dis в любом сгустке) с любым означиванием  $V$ for для переменных $x_i$ из данной формулы $\varphi$.
 Берем любое состояние $a \in F$.


 Рассмотрим случай когда $(F,a) \Vdash_V \neg \Diamond \Box \varphi $.
По определению подстановки  $\sigma_3$, она является унификатором для формулы $\varphi$ в логике,
поэтому

\[ \forall b \in F, \ (F,b) \Vdash_V \sigma_3(\varphi)) \ \mbox{и соответсвенно} \ \forall b \in F, \ (F,b) \Vdash_V \sigma(\varphi)).\]

Допустим теперь что  $(F,a) \Vdash_V  \Box \varphi $. Тогда подстановка $\sigma$ не меняет истинностных значений переменных $x_i$ в сравнении с их истинностными значениями при оригинальном означивании $V$. Поэтому

\[ (F,a) \Vdash_V  x_i \  \lri \ (F,a) \Vdash_V  \sigma(x_i), \ \forall b \geq a  \
(F,b) \Vdash_V  x_i \  \lri \ (F,b) \Vdash_V  \sigma(x_i), \]
следовательно

\[ (F,a)  \Vdash_V  \sigma(\Box \varphi).\]

Осталось рассмотреть случай когда


\[ (F,a)  \Vdash_V \neg \Box \varphi \wedge \Diamond \Box  \varphi .\]

Пусть $C(i)$ это наименьший сгусток где формула $\Box  \varphi$  истинна при
оригинальном означивании $V$, пусть $Dis(i)$ и $Dis(i-1)$  это два выбранных любых состояния типа   $Dis$ из $C(i)$ и $C(i-1)$ соответственно. Тогда для любой $x_i \in Var(\varphi)$ ввиду того что состояния  $Dis(i)$ и $Dis(i-1)$    являются выключенными имеет место

\[ (F,Dis(i))  \Vdash_V \neg x_i,     \&   \
  (F,Dis(i-1))  \Vdash_V \neg x_i.   \]
Используя это и вновь выключенность состояний $Dis(i)$ и $Dis(i-1)$ (ограничения на работу агентных операций $R_j$) прямой индукцией на длину формул легко проверить, что для любой булевой формулы $\alpha$  построенной из переменных $x_i$


\medskip

{\bf Лемма 20.}
\[   (F,Dis(i))  \Vdash_V \alpha    \ \lri \
  (F,Dis(i-1))  \Vdash_V \alpha.   \]
\medskip

\medskip

Кроме того верна

\medskip

{\bf Лемма 21.}
 Для любого состояния $g$ типа Dis из любого сгустка $(C(j)$ модели $М$ и любого означивания $V_2$ на М, и любой формулы  $ \beta $ из
 $Sub(\Box \varphi)$

\[ (F,g) \Vdash_{V_2}
\bigwedge_{\beta \in Sub(\Box \varphi) } ([\beta \ii \bigwedge_{j\in J} K_j \beta] \wedge
[\bigwedge_{j\in \beta \in Sub(\Box \varphi)}[K_j \beta \ii \beta]). \]

\medskip

Доказательство прямо следует из определения агентных отношений достижимости $R_j$  на состояниях типа Dis.

\medskip

Из этих двух лемм, прямой индукцией по длине формул $\alpha$ выводится


\medskip

{\bf Лемма 22.}
   Для любой формулы $\alpha$ из $Sub((\Box \varphi))$, построенной из переменных $x_i$

\[ (F,Dis(i))  \Vdash_V \sigma(\alpha)    \ \lri \
  (F,Dis(i-1))  \Vdash_V \sigma(\alpha).   \]

\medskip

Для сгустков $C(j)$ расположенных ниже $C(i-1)$ доказательство предыдущей леммы то же как и предыдущей леммы, так как в таких сгустках при подстановке $\sigma$ переменные имеют то же означивание после применения подстановки  $\sigma$   как и в $C(i-1)$.

Тем самым  мы доказали что
подстановка $\sigma$ построенная нами и является  унификатором для
$\varphi$. Проективность этой подстановки очевидна.

Теорема доказана

\bigskip






\begin{thebibliography}{90}

\bibitem{faa2} {\it Ronald Fagin, Joseph Y. Halpern, Yoram Moses and Moshe Vardi)}
Reasoning About Knowledge, MIT, 1995}).



\bibitem{rraa2z} {\it  V. V. Rybakov } {\it Refined common knowledge logics or logics of common information
{\it
 Archive for mathematical Logic 42 (2), 2003}, 179-200.}



\bibitem{ar1} {\it S. Artemov}  Evidence-Based Common Knowledge,
(Technical Report TR-2004018 CUNY Ph.D. Program in Computer Science, revised version)

\bibitem{ar2}
  {\it S. Artemov} Explicit Generic Common Knowledge}, Lect/ Notes in CS,  LFCS 2013: Logical Foundations of Computer Science 2013, pp 16–28Cite as

\bibitem{ar3}  {\it S. Artemov}
{ Justification awareness
} Journal of Logic and Computation 30 (8), 2020, 1431-1446

\bibitem{ry2}
{\it  V Rybakov Temporal Multi-Agent’s Logic, Knowledge, Uncertainty, and Plausibility}
Agents and Multi-Agent Systems: Technologies and Applications, LNCS, 2021,  2005 -  2014.




\bibitem{ba2}
Baader F., Küsters R. {\em Unification in a description logic with transitive closure of roles.} In: Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2001. Vol. 2250. LNCS, Springer (2001),  217 -- 232.



\bibitem{r4}
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{rint}
Rybakov V.V. {\em  Rules of Inference with Parameters for Intuitionistic
logic.}-  J. of Symbolic Logic, 57 (3) (1992),  912 -- 923.


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


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

\bibitem{08с}
 Rybakov V. V.Projective formulas and unification in linear temporal logic LTLU,
V Rybakov
Logic Journal of the IGPL 22 (4), (2014), 665-672.

\bibitem{08a} Rybakov V. V. {\em Non-transitive linear temporal logic and logical knowledge operations},
Journal of Logic and Computation 26 (3), Oxford Press, 2016,  945-958

\bibitem{vr11x}
Rybakov V.V. {\em
Nontransitive temporal multiagent logic, information and knowledge,
deciding algorithms}, Siberian. Math. J.,
58,
no 5, (2017), 875–886.


\bibitem{vr11y}
Rybakov V.V.,
{\em Multiagent temporal logics with multivaluations},
Siberian. Math. J.,
59,
no 4, (2018),
710–720.

\bibitem{vr11z}
Rybakov V.V.,
{\em Branching time agents’ logic, satisfiability problem by rules in reduced
form},
 Siberian. Electron. Math. Izv.,
16,
(2019), 1158-–1170.

\bibitem{08с}
 Rybakov V. V. {\em Projective formulas and unification in linear temporal logic LTLU},
Logic Journal of the IGPL, Oxford Press< 22 (4), (2014), 665-672.

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


\bibitem{g1}
Ghilardi S. {\em  Unification, finite duality and projectivity in
varieties of Heyting algebras,}  Annals of Pure and Applied Logic, 127(1-3),
(2004),  99 -- 115.



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




\end{thebibliography}

\end{document}

\bibitem{dz1}
Wooldridge. {\em ``An Automata-theoretic
approach to multi-agent planning'', }  in:
 Proceedings of the First European Workshop
 on Multi-agent Systems (EUMAS 2003), Oxford
 University, December 2003.

\bibitem{dz2}
Belardinelli F. and Lomuscio A. {``Interactions
between Knowledge and Time in a First-Order
Logic for Multi-Agent Systems: Completeness Results'',}
 Journal of Artificial Intelligence Research,
 vol. 45,  1--45 (2012).




[1] Gabbay D.M., Hodkinson I.M.
and Reynolds M.A.
  {\em ``Temporal
Logic'',} - { Mathematical
Foundations and Computational Aspects,}
vol. 1., Clarendon Press,
Oxford (1994).

\medskip

[2] Gabbay D.M., Hodkinson I.M.
 {\em ``An axiomatization of
the temporal logic with Until
and Since over the real numbers'',}
{Journal of Logic and Computation},
vol. 1, 229 -- 260 (1990),  229 -- 260.

\medskip

[3]
 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).



[4]
 Wooldridge M. and  Lomuscio A.
 {\em ``Multi-Agent VSK Logic'',}
 in: Proceedings of the Seventh European
 Workshop
 on Logics in Artificial Intelligence (JELIAI-2000), 2000,  Springer-Verlag, September 2000.

\medskip

[5]
Wooldridge. {\em ``An Automata-theoretic
approach to multi-agent planning'', }  in:
 Proceedings of the First European Workshop
 on Multi-agent Systems (EUMAS 2003), Oxford
 University, December 2003.

\medskip

[6]
 Wooldridge M., Huget M.P.,  Fisher M.,
 and Parsons S., ``Model Checking Multi-Agent
 Systems: The MABLE Language and Its Applications'',
 International Journal on Artificial Intelligence
 Tools, vol.15. no. 2, 195 -- 225 (2006).

\medskip



[7]
Belardinelli F. and Lomuscio A. {``Interactions
between Knowledge and Time in a First-Order
Logic for Multi-Agent Systems: Completeness Results'',}
 Journal of Artificial Intelligence Research,
 vol. 45,  1--45 (2012).


\medskip



[8] Emerson, E. A.; Halpern, J. Y. (1985). "Decision procedures and expressiveness in the temporal logic of branching time". Journal of Computer and System Sciences. 30 (1): 1–24. doi:10.1016/0022-0000(85)90001-7.

\medskip


[9] Clarke, E. M.; Emerson, E. A. & Sistla, A. P. (1986). "Automatic verification of finite-state concurrent systems using temporal logic specifications". ACM Transactions on Programming Languages and Systems. 8 (2): 244–263. doi:10.1145/5397.5399.

\medskip


[10]  J. Carmo and A. Sernadas. Branching vs linear logics yet a gain.
Formal Aspects of Computing, 2:24–59, 1990, 1170.

\medskip

[11] V.Rybakov,
Non-transitive linear temporal logic and logical knowledge operations
, J. of
Logic Comput., Oxford Press, 26
:3 (2016), 945–958. Zbl 1403.03028

\medskip


[12]
 V. Rybakov, ``Intransitive Temporal
 Multi-agency Logic, Knowledge and Uncertainty,
 Plausibility'', in:
International Symposium on Logical
Foundations of Computer Science,
Lecture Notes in Computer Science,
2016, pp. 364-375, vol.
 9537.


\medskip

[13]
V.V. Rybakov,
Nontransitive temporal multiagent logic, information and knowledge,
deciding algorithms
, Sib. Math. J.,
58
:5 (2017), 875–886. Zbl 1420.03060

\medskip


[14]
V. Rybakov,
Multiagent temporal logics with multivaluations
, Sib. Math. J.,
59
:4 (2018),
710–720. Zbl 06976648

\medskip

[15]
V.  Rybakov,
Linear Temporal Logic with Non-transitive Time, Algorithms for
Decidability and Verification of Admissibility
, in
Outstanding Contributions to Logic
,
Springer, 2018, 219–243. Zbl 1429.03074

\medskip

[16]
V. Rybakov,
Temporal multi-valued logic with lost worlds in the past
, Sib. Electron.
Math. Izv.,
15
(2018), 436–449. Zbl 06931667
[25]

\medskip

[17]
V. Rybakov,
Branching time agents’ logic, satisfiability problem by rules in reduced
form
, Sib. Electron. Math. Izv.,
16
(2019), 1158–1170. Zbl 07122035

\medskip


[18] Rybakov V. V.
Temporal logic with accessibility temporal relations generated by time states themselves,
Sib. Electron. Math. Izv., 17, (2020), pp. 923-932.
 10.33048/semi.2020.17.068

\medskip

[19] S. Babenyshev, V. Rybakov,
Linear Temporal Logic LTL: Basis for Admissible Rules
, Journal
of Logic and Computation, Oxford Press,
21
:2 (2011), 157–177. Zbl 1233.03026

\medskip

[20]
V.V. Rybakov,
Logical Consecutions in Discrete Linear Temporal Logic
, J. of Symbolic
Logic,
70
:4 (2005), 1137–1149. Zbl 1110.03010


%\end{thebibliography}

\end{document}



\end{document}


\end{document}



\newpage

Работа касаются решения  проблем унификации (см. \cite{ba2,ba3,ba4})и распознавания допустимых правил вывода (см. \cite{r4,rint}) в модальных и неклассических логиках,
в много-агентных временных логиках с участками потерянного времени и динамических отношениях временной достижимости порождаемых самими временными состояниями. Результаты существенно используют технику проективных формул предложенную ранее Гиларди в 1997 году (см. \cite{r10,g1})


Цель работы - решение проблемы унификации и допустимости в много-агентных логиках с линейным временем и динамическими отношениями временной достижимости.

 Язык наших логик включает язык булевой пропозициональной логики и логические операции агентов $U_j$ (где  $j \in J$  и  $J$  это фиксированное конечное множество имен агентов). Правила образования формул стандартные: -- любая пропозициональная переменная -- формула, если $\varphi$   и  $\psi$  формулы то
$\varphi \wedge \psi, \varphi \vee \psi, \varphi \rightarrow \psi, \varphi U_j \psi, \neg \varphi
   $ тоже формулы. Формула  $\varphi U_j \psi$, выражает свойство:  $\varphi $ всегда остается истинной до того как  $\psi$ становится первый раз истинной в восприятии агента  $j$.

Опишем модели много-агентных логик. Любой фрейм базируется на множестве $N$  всех натуральный чисел
и стандартном отношении
 $\leq$  на $N$ . Для любого агента $j \in J$, $X_j$ является некоторым подмножеством множества
   $N$, оно обозначает множество временных состояний не доступных для агента  $j$ (состояния потерянного времени).


  {\bf Определение 1. } Фрейм $F := \langle N, \leq, X_j, j \in J \rangle$ называется фреймом линейного времени с забытыми временами
 $X_j, j \in J \rangle$.


  {\bf Определение 2.  } {\it Модель $M$ на фрейме
 $F$ определяется заданием означивания
 $V$ на $F$ некоторого множества пропозициональных переменных  $p$, где
$V(p) \subseteq   N $, все состояния из $V(p)$ - те где $p$ считается истинным относительно  $V$.
$T(M) := N$ считается основным множеством модели $M$.}

\medskip
Любое такое означивание расширяется на все формулы следующим образом.

\medskip

{\bf Определение 3.} Для всех $a\in T(M)  $:

\[  \left(F,a\right) \Vdash_{V}  p  \ \Leftrightarrow \ \  p \in V(p); {\mbox{ для всех булевых логических связок определение обычное, и } \]


 Для формул  $ \varphi {\bf U}_j \psi$  определение следующее (напомним что ${\bf U}_0 $
 логическая операция для глобального времени).

\[\left(F,a\right) \Vdash_{V} \left(\varphi \ {\bf U}_0 \ \psi\right) \  \Leftrightarrow  \\]

\[  (\exists  b \in T(M) \ \left[
 \left(a \leq b\right)\wedge
\left(\left(F,b\right)\Vdash_{V} \psi\right) \ \& \]
\[\forall c (a \leq  c < b, c \neq b ) \ \ri \
\left( F,c\right)\Vdash_{V} \varphi \right]]), \]



\[(*) \left(F,a\right) \Vdash_{V} \left(\varphi \ {\bf U}_j \ \psi\right) \ (j \neq 0) \Leftrightarrow \]

\[\left(  [[\left(F,a
\right)\Vdash_{V} \psi \right)]] \vee  \left(\left(F,a\right)\Vdash_{V} \varphi \right) \ \& \
 \(\exists  b \in T(M) (b \notin X_j \& ( a < b )  \ \& \]
 \[
 \left(\left(F,b\right)\Vdash_{V} \psi\right) \ \ \& \ \
  \forall c (a <  c < b \ \ \& \ c \notin X_j,  c  ) \ \Rightarrow
\left( F,c\right)\Vdash_{V} \varphi \right]]). \]


  Требование $(F,a\right)\Vdash_{V} \varphi \right$  в (*) выше фиксирует состояние, где вычисление истинности начинается.

  \medskip

{\bf Определение 4. } {\it Логика $L$ это множество всех формул истинных на всех состояниях всех возможных моделей.}


\medskip

Введение этой логике расширяет тематику унифицируемости на многоагентные логики появление которых во многом связано с инженерными задачами возникающие в исследованиях по многоагентным системам в задачах искусственного  интеллекта.

%ПЕРЕНЕСТИ {\bf Definition 5.} \label{d}  {\it For any class of Kripke frames $K$, the modal logic $L(K)$ %of $K$ is
%the set of all formulas which are true at any state of any frames foe any valuation $V$ on this frame.}



\section{\bf Унификация и Допустимость}


Унификация возникла в математической логике и информатике как задача идентификации термов через подстановку вместо переменных (что может быть интерпретировано как решение символьных уравнений), (см. например Баадер \cite{ba2,ba3,ba4}). В дальнейшем эта задача была расширена на случай логической унификации - когда вместо термов (формул) можно применять все эквивалентные им в той или иной логической системе  Кратко напомним необходимые определения и технику. Предполагаем логику $L$(в частности нашу введенную выше) зафиксированной и  $For_L$ это просто множество всех формул в языке этой логики и $P$  - множество некоторых переменных.

Подстановка для $P$ это некоторое отображение $\varepsilon$  множества $P$ в
$For_L$. Любая подстановка
 $\varepsilon$ расширяется на множество всех формул построенных из $P$
как указано ниже

\[\varepsilon
(\ppp(x_1, \dots , x_n)) := \ppp(\varepsilon(x_1), \dots ,
\varepsilon(x_n))\].



{\bf Definition 5. } {\it Формула
$\ppp$ является унифицируемой в логике $L$ если существует подстановка
$\varepsilon$ (называемая унификатором для $\ppp$) такая что $
\varepsilon(\ppp) \in L$.
}
%Now we recall the basic definition of our paper:

\medskip


{\bf Definition 6. } {\it \label{lu1} {\it
Унификатор $\varepsilon$ (для формулы  $\ppp$ в логике  $L$) является более общим
чем унификатор  $\varepsilon_1$, если существует подстановка
$\delta$ такая что для любой переменной  $x$, $[\varepsilon_1(x) \equiv
\delta(\varepsilon(x))] \in L$. }

\medskip



%\begin{definition} \label{lu1} {\em
%A substitution $ \varepsilon$ is a unifier for a formula $\ppp$ in $\llll$ if
%$\varepsilon(\ppp) \in \llll$.  A formula $\ppp$ is unifiable in
%$\llll$ if it has a unifier. A unifier $\varepsilon$ is more general
%than a unifier $\varepsilon_1$ iff there is a substitution $\delta$
%such that for any letter $x$, $\varepsilon_1(x) = \delta(\varepsilon
%(x))$.}
%\end{definition}


%Since the logic $\llll$ is decidable, to check unifiability a formula
%in $\llll$, is the reasonably easy task: it is sufficient to use only
%ground substitutions: mappings of variables in the set $\{\bot,
%\top\}$.


{\bf Definition 7. } {\it Множество унификаторов
  $CU$ для данной формулы $\ppp$ в логике $L$ является некоторым полным множеством унификатором
если оно обладает следующим свойством. Для любого унификатора
$\sigma$ для $\ppp$ в $L$, существует  $\sigma_1$ из $CU$, где $\sigma_1$ более общий чем
$\sigma$. Если одноэлементное множество $\{\sigma_p\}$ полное множество унификаторов для  $\ppp$ то  $\sigma_p $ называется наиболее общим ун6ификатором для for $\ppp$.
}}

\medskip

Если логика имеет операцию  $\Box$ - необходимо - выражаемую в логике (у нас например $\Box \ppp =
 T U_0 \ppp$) то свойство проективности может быть выражено следующим образом.

\medskip

{\bf Definition 8. } {\it  Формула  $\ppp$ называется проективной для логики  $L$
если существует подстановка $\sigma$ являющаяся унификатором для $\ppp$ (называемая проективной) такая что $\Box \ppp \ii [ x_i \equiv \sigma (x_i)] \in L$ для любой переменной  $x_i$ из $\ppp$.
}

\medskip



{\it  Несложно заметить, что если $\sigma_p$ проективная подстановка для формулы
   $\ppp$  в логике $L$, то $\{\sigma_p\}$ полное множество унификаторов для $\ppp$ (i.e. $\sigma_p $ наиболее общий унификатор для $\ppp$).}
}

\medskip


{\bf Theorem 9.} {\it Если логика $L$ является разрешимой и существует алгоритм проверяющий унифицируемость любой данной формулы  в $L$ и любая унифицируемая формула проективна и существует алгоритм  строящий по любой унифицируемой формуле ее проективный унификатор то проблема допустимости в правил вывода в логике   разрешима}

Эта простая (почти очевидная) теорема позволяет решить проблему допустимости в логиках обладающих свойством проективности для которых применение существующей ранее техники является не очень эффективным. Конечно совсем не все интересные логики обладают свойством проективности (например для логики $S4$ Гиларди (Gilardi) использовал свойство конечной проективной аппроксимации; Рыбаков [4,5] применял свойство насыщенности по накрытием. Но если это свойство присутствует а логики содержательны и интересны, то найти компактные общие теоремы решающее целый класс таких проблем выглядит очень привлекательным.

\medskip


\section{\bf Унифицируемость и Допустимость через Проективность}

Мы применяем здесь напомненную в предыдущей секции технику исследования унифицируемости через проективные формулы приложенную Гиларди (см. \cite{r10,g1}) и развитую нами ранее технику решения проблемы выполнимости в многоагентных логиках.
(см. [12, ---, 18]). Исследуем логику $L$   введенную нами выше.


\medskip

{\bf Lemma 10} {\it Существует алгоритм проверяющий унифицируемость любой данной формулы
в $L$  и в случае унифицируемости строящий ее унификатор из $ \top, \bot$.}

\medskip


{\bf Lemma 11.} {\it Существует алгоритм проверяющий  выполнимость любой данной формулы в $L$.  }

\medskip

Базируюсь на технике из [17,18] и доложенной в предыдущей секции мы доказываем следующую  теорему.


\medskip

{\bf Теорема 12}.{ \it Любая формула унифицируемая в
 $L$  проективна и существует алгоритм конструирующий для любой унифицируемой формулы ее некоторый проективный унификатор.}

 \medskip

Этот результат расширяет результаты из  \cite{dz} и из Рыбаков [13] о проективности унифицирумых формул в модальной логике $S4.3$  и линейной временной логике $LTL$ с удаленным оператором NEXT, соответственно,  на многоагентные временные логики.
 Используя Теорему 12 мы решаем проблему распознавания допустимости правил вывода в $L$.

\medskip


{\bf Теорема 13.} {\it Проблема распознавания допустимости правил вывода в $L$     алгоритмически разрешима.
 }

\medskip

Эта теорема расширяет теоремы из Рыбаков [5,6,7]
 о решении проблемы допустимости в линейной временной логике
 LTL  на линейные временные логики с мультиагентными операциями с потерянным временем

\medskip

\section{\bf Логики с Динамическими Отношениями Временной Достижимости Агентов}

 В этой секции мы описываем наш основной новый результат полученный в необычных новых системах с динамической временной достижимостью. Мы расширяем временные модели, предполагая что в абсолютно любом временном состоянии любой агент имеет свое восприятие времени и его протяженность своя, причем в любом состоянии и для любого агента вне зависимости от других состояний.

\medskip


{\bf Определение 14.}
{\it  Линейный временной не-транзитивный фрейм это набор


\[{\cf} := \langle N, \{ R_x \mid  x \in  N \},
   \rangle, \mbox{ такой что }\]
  для всех  $x \in N$, $R_x$ является стандартным линейном порядком на интервале
$[x, a_x]$ для некоторого $a_x \geq x, a_x \in N$, также возможно что $R_x$ это
линейный порядок на всем интервале
 $[x, \infty)$}. }


\medskip

В этом определении может случится, что
 $x R_x a_x$, $ y \in (x,a_x)$  и $not (y R_y a_x)$. То есть $y$ является состоянием расположенным ранее чем  $x$ но $y$ помнит даже меньше чем $x$ помнит. Кроме того понятно что все временные отношения достижимости вместе образуют не-транзитивное отношение: может случится, что  $x R_x a_x$, $x < y < a_x$, то есть $(a R_x y)$, $(y R_y a_y) $ но $not (x R_y a_y)$.

  Таким образом, любое состояние $ x\in N$ порождает его {\em собственное время}  $R_x$.
  Поэтому время становится динамический субстанцией меняющейся от состояния к состоянию. В то же время глобальной время $R_{x,0}$ - временная достижимость агента $0$ -- остается полным $\leq$ на $N$ как и ранее.

Модель $\cm$ на любом фрейме  $\cf$ определяется как и ранее путем введения некоторого означивания
    $V$ на $\cf$:  для некоторого множества пропозициональных переменных $p$ :
$V(p) \subseteq   N $. Далее мы можем ввести множества забытых времен $X_j$ для агентов $j$ как и ранее.


После этого  $V$ может быть расширено на все формулы как и ранее, но только используя при вычислении истинности формул вида $ \ppp U_j \psi $ (при   $j \neq 0$) на любом состоянии $x$ отношение $R_x$ вместо  $\leq$.





Далее мы определяем логику $L_1$ стандартным образом --- как множество всех формул истинных на всех состояниях всех возможных моделей.
Используя технику и результаты предыдущих секций и наши результаты из \cite{vr11x,vr11y,vr11z,08b}
мы доказываем наш основной результат.

\medskip

{\bf Теорема 15}.{ \it Любая формула унифицируемая в $L_1$
   проективна; существует алгоритм строящий по любой унифицируемой формуле ее проективный унификатор.}

\medskip

Как и ранее из этого выводится

\medskip

{\bf Теорема 15.} {\it Проблема распознавания допустимых правил в логике $L_1$ разрешима. }

\medskip



%{\Large \sc Список литературы}

%\begin{thebibliography}{10}



\begin{thebibliography}{90}



\bibitem{ba2}
Baader F., Küsters R. {\em Unification in a description logic with transitive closure of roles.} In: Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2001. Vol. 2250. LNCS, Springer (2001),  217 -- 232.

\bibitem{ba3}
Baader F., Narendran P. {\em
Unification of concept terms in description logics.} Journal of Symbolic Computation, 31 (2001), 277 -- 305.


\bibitem{ba4}
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{r4}
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{rint}
Rybakov V.V. {\em  Rules of Inference with Parameters for Intuitionistic
logic.}-  J. of Symbolic Logic, 57 (3) (1992),  912 -- 923.


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


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

\bibitem{08с}
 Rybakov V. V.Projective formulas and unification in linear temporal logic LTLU,
V Rybakov
Logic Journal of the IGPL 22 (4), (2014), 665-672.

\bibitem{08a} Rybakov V. V. {\em Non-transitive linear temporal logic and logical knowledge operations},
Journal of Logic and Computation 26 (3), Oxford Press, 2016,  945-958

\bibitem{vr11x}
Rybakov V.V. {\em
Nontransitive temporal multiagent logic, information and knowledge,
deciding algorithms}, Siberian. Math. J.,
58,
no 5, (2017), 875–886.


\bibitem{vr11y}
Rybakov V.V.,
{\em Multiagent temporal logics with multivaluations},
Siberian. Math. J.,
59,
no 4, (2018),
710–720.

\bibitem{vr11z}
Rybakov V.V.,
{\em Branching time agents’ logic, satisfiability problem by rules in reduced
form},
 Siberian. Electron. Math. Izv.,
16,
(2019), 1158-–1170.

\bibitem{08с}
 Rybakov V. V. {\em Projective formulas and unification in linear temporal logic LTLU},
Logic Journal of the IGPL, Oxford Press< 22 (4), (2014), 665-672.

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


\bibitem{g1}
Ghilardi S. {\em  Unification, finite duality and projectivity in
varieties of Heyting algebras,}  Annals of Pure and Applied Logic, 127(1-3),
(2004),  99 -- 115.



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




\end{thebibliography}

\end{document}

\bibitem{dz1}
Wooldridge. {\em ``An Automata-theoretic
approach to multi-agent planning'', }  in:
 Proceedings of the First European Workshop
 on Multi-agent Systems (EUMAS 2003), Oxford
 University, December 2003.

\bibitem{dz2}
Belardinelli F. and Lomuscio A. {``Interactions
between Knowledge and Time in a First-Order
Logic for Multi-Agent Systems: Completeness Results'',}
 Journal of Artificial Intelligence Research,
 vol. 45,  1--45 (2012).




[1] Gabbay D.M., Hodkinson I.M.
and Reynolds M.A.
  {\em ``Temporal
Logic'',} - { Mathematical
Foundations and Computational Aspects,}
vol. 1., Clarendon Press,
Oxford (1994).

\medskip

[2] Gabbay D.M., Hodkinson I.M.
 {\em ``An axiomatization of
the temporal logic with Until
and Since over the real numbers'',}
{Journal of Logic and Computation},
vol. 1, 229 -- 260 (1990),  229 -- 260.

\medskip

[3]
 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).



[4]
 Wooldridge M. and  Lomuscio A.
 {\em ``Multi-Agent VSK Logic'',}
 in: Proceedings of the Seventh European
 Workshop
 on Logics in Artificial Intelligence (JELIAI-2000), 2000,  Springer-Verlag, September 2000.

\medskip

[5]
Wooldridge. {\em ``An Automata-theoretic
approach to multi-agent planning'', }  in:
 Proceedings of the First European Workshop
 on Multi-agent Systems (EUMAS 2003), Oxford
 University, December 2003.

\medskip

[6]
 Wooldridge M., Huget M.P.,  Fisher M.,
 and Parsons S., ``Model Checking Multi-Agent
 Systems: The MABLE Language and Its Applications'',
 International Journal on Artificial Intelligence
 Tools, vol.15. no. 2, 195 -- 225 (2006).

\medskip



[7]
Belardinelli F. and Lomuscio A. {``Interactions
between Knowledge and Time in a First-Order
Logic for Multi-Agent Systems: Completeness Results'',}
 Journal of Artificial Intelligence Research,
 vol. 45,  1--45 (2012).


\medskip



[8] Emerson, E. A.; Halpern, J. Y. (1985). "Decision procedures and expressiveness in the temporal logic of branching time". Journal of Computer and System Sciences. 30 (1): 1–24. doi:10.1016/0022-0000(85)90001-7.

\medskip


[9] Clarke, E. M.; Emerson, E. A. & Sistla, A. P. (1986). "Automatic verification of finite-state concurrent systems using temporal logic specifications". ACM Transactions on Programming Languages and Systems. 8 (2): 244–263. doi:10.1145/5397.5399.

\medskip


[10]  J. Carmo and A. Sernadas. Branching vs linear logics yet a gain.
Formal Aspects of Computing, 2:24–59, 1990, 1170.

\medskip

[11] V.Rybakov,
Non-transitive linear temporal logic and logical knowledge operations
, J. of
Logic Comput., Oxford Press, 26
:3 (2016), 945–958. Zbl 1403.03028

\medskip


[12]
 V. Rybakov, ``Intransitive Temporal
 Multi-agency Logic, Knowledge and Uncertainty,
 Plausibility'', in:
International Symposium on Logical
Foundations of Computer Science,
Lecture Notes in Computer Science,
2016, pp. 364-375, vol.
 9537.


\medskip

[13]
V.V. Rybakov,
Nontransitive temporal multiagent logic, information and knowledge,
deciding algorithms
, Sib. Math. J.,
58
:5 (2017), 875–886. Zbl 1420.03060

\medskip


[14]
V. Rybakov,
Multiagent temporal logics with multivaluations
, Sib. Math. J.,
59
:4 (2018),
710–720. Zbl 06976648

\medskip

[15]
V.  Rybakov,
Linear Temporal Logic with Non-transitive Time, Algorithms for
Decidability and Verification of Admissibility
, in
Outstanding Contributions to Logic
,
Springer, 2018, 219–243. Zbl 1429.03074

\medskip

[16]
V. Rybakov,
Temporal multi-valued logic with lost worlds in the past
, Sib. Electron.
Math. Izv.,
15
(2018), 436–449. Zbl 06931667
[25]

\medskip

[17]
V. Rybakov,
Branching time agents’ logic, satisfiability problem by rules in reduced
form
, Sib. Electron. Math. Izv.,
16
(2019), 1158–1170. Zbl 07122035

\medskip


[18] Rybakov V. V.
Temporal logic with accessibility temporal relations generated by time states themselves,
Sib. Electron. Math. Izv., 17, (2020), pp. 923-932.
 10.33048/semi.2020.17.068

\medskip

[19] S. Babenyshev, V. Rybakov,
Linear Temporal Logic LTL: Basis for Admissible Rules
, Journal
of Logic and Computation, Oxford Press,
21
:2 (2011), 157–177. Zbl 1233.03026

\medskip

[20]
V.V. Rybakov,
Logical Consecutions in Discrete Linear Temporal Logic
, J. of Symbolic
Logic,
70
:4 (2005), 1137–1149. Zbl 1110.03010


%\end{thebibliography}

\end{document}



\end{document}

\section{Введение}

Современные исследования в математической логике и ее применениях в информатике включают
 исследования временной логики и ее вариантов связанных с различными представлениями структуры временных потоков. Значительная часть работ в этой области в информатике рассматривает время как важный ресурс связанный с эффективностью и надежностью программного обеспечения.

 Исследования по многоагентной логике включают временной ресурс как важный компонент и опираются на
 модальности  интерпретированные
через агентные отношения достижимости.
Временная логика в терминах
 математической и философской логики
  исследовалась Артуром Прайором  в конце  1950-х.
 С тех пор она остается активной областью в
  информатике,
 работах по искусственному интеллекту.
 (см. --  Gabbay and Hodkinson [1,2,3]).
 Один важный частный случай таких логик -
 линейная темпоральная логика
 ${{\cal LT \hspace*{-0.05cm}L}}$,
  была использована
 в анализе протоколов вычислений,
 верификации корректности.
 Многоагентная логика может быть интерпретирована как модальная логика
 с модальностями интерпретированными как операции знания, осведомленности агентов
 (см. Woldridge, Lomuscio  [4],
Woldridge [5,6], Lomuscio et al [7])).
 Получение информации,
 взаимодействие агентов  -- происходит
в течении определенного интервала времени,
 и протяженность этого интервала может
 быть существенна для оценки надежности полученного знания.

 В инновационных работах по временной логике в информатике изначально время трактовалось как
 линейное отношение, и это было хорошо для первоначального применения. Однако же вычислительные процедуры часто имеют структуру связанную с разветвлением вычислительных потоков -- и было формализовано и применена концепция ветвящегося времени. Например была введена логика $CTL$ --
 логика ветвящегося времени вычислений, предполагающее различные потоки вычислений  - их возможность разветвится в любой точке вычисления (см. например Emerson at el [8], [9], [10]).

 Далее было подмечено что допущение о транзитивности отношения временной достижимости является слишком сильным и что историческая практика как и научные исследования часто помечают что течение времени не всегда транзитивно. В частности автор, впервые для не него, обратил на это внимание в работе Рыбаков [11] где исследовал временную интервальную логику для нетранзитивного но квазилинейного времени и доказал ее разрешимость.
	 Моделирование мультиагентности
в случае нетранзитивного времени было предпринято в
	 Rybakov [12].


Дальнейшие работы были посвящены исследованию моделей и логик с интервалами потерянного времени
-- пробелами в информации, и таких логик с введенными отношениями временной достижимости для агентов (очевидно что она может быть разной) - см. Рыбаков [13,14,15,16]. Причем были исследованы и случаи с разными отношениями временной достижимости агентов и одним и тем же означиванием истинности для фактов и различным - для разных агентов - см. [14,16].

Недавно автор начал исследование нетранзитивной временной логики с ветвящимся временем и мультиагентными отношениями - см. [17] - и доказал разрешимость этой логики.
В этой работе применен подход исследование ветвящегося времени с элементами интервальной логики -- когда все отношения временной достижимости агентов равномерно ограничены -- находятся в интервале объективной временной достижимости. Снять это ограничение автор не смог по техническим причинам и общее решение не было найдено. В этой нашей статье мы решаем эту проблему и находим решение в  общем случае.
В заключительной части статьи приводятся некоторые
 интересные открытые проблемы.



\section{Вводные Определения и Обозначения}

Объектом нашего исследования в этой статье будет временная логика с семантическим базисом состоящим из моделей базирующихся на ветвящемся времени и  отношением временной  достижимости агентов порождаемом в каждом текущем временном состоянии.
Начнем с описания логического языка, базируется на потенциально бесконечном множества $Pr$ пропорциональных переменных и использует стандартные булевы логические связки
$\wedge, \vee, \rightarrow, \neg $ и временные связки - бинарные $U_j$ где $j \in J$ и $J$- конечное
множество обозначений имен для агентов и унарная связка $Nxt$ -  завтра.

Правила образования формул стандартные:
любая пропозициональная переменная - формула; если $\varphi$   и  $\psi$  формулы то
$\varphi \wedge \psi, \varphi \vee \psi, \varphi \rightarrow \psi, \varphi U_j \psi, \neg \varphi,
 Nxt \varphi$
  тоже формулы. Формула $\varphi U_j \psi$, служит обозначением для свойства   $\varphi $  всегда остается истинной до тех пор пока $\psi$  не станет истинной со  временем в восприятии агента $j$;   $Nxt \ \varphi$ значит $\varphi$   будет истинной в непосредственно последующем (NEXT) временном состоянии.

Теперь опишем модели и фрейм ветвящегося времени. Временной фрейм это множество временных состояний с бинарным
 объективным (глобальным) бинарным отношением временной достижимости (которое само по себе на зависит от восприятия агентов).

 Обычно в логике действий и временной логике действий время рассматривается как линейное в прошлом и потенциально ветвящееся в будущем (отражая потенциально различное развитие событий в будующем). Мы будем придерживаться этой традиции. Формально этот подход формализуется следующим образом;
начнем с определение фрейм ветвящегося времени.
Каждый фрейм ветвящегося времени состоит из состояний (states or worlds -- as it is cold in Kripke semantics) начинается с корня $\{ a_{1,1}\}$  (так сказать начала времен).

Пусть $S_1 := \{ a_{1,1}\}$ - это фрейм глубины $1$, $Sl_1 := \{ a_{1,1}\}$ -- его первый временной слой. Пусть фрейм $S_k$ глубины $k$ уже построен и $Sl_k$ - его $k$-й временной слой; для каждого $a\in Sl_k$, выберем некоторое конечное множество


\[Sl_{a,k+1} := \{a_{k,k_1}, \dots , a_{k,k_m} \}\]
новых временных состояний -- называем их временными состояниями непосредственно следующими за $a$  и
задаем отношение временного следования:

\[ a \prec c$ \mbox{ \ для всех \ } c \in Sl_{a,k+1} . \]
 Состояния из $Sl_{a,k+1}$ являются (так сказать)  состояниями завтра для
  $a$
и время из состояния  $a$ ветвится во все состония $c$   из $Sl_{a,k+1}$.

Поэтому $m$ -- число состояний в $Sl_{a,k+1}$ -- называем ветвлением
состояния $ a $; обозначаем его через  $Br(a)$.
Пусть
 \[ S_{k+1} :=  \bigcup_{a \in Sl_k}} Sl_{a, k+1} \cup S_k  \ \ \mbox{  и  } \ \
 T(M) := \bigcup_{k \in N,  k \leq m} S_k, \]
  далее полагаем, что $\preceq_*$ есть рефлексивное бинарное отношение достижимости на состояниях из $T(M)$, полученное
конкатенацией всех отношений $\preceq$ непосредственного временного следования введенного выше.
Т.е. фреймы $T(M)$ конечны по определению.
 Временная цепь $Ch$ в $T(M)$ это любое множество $Ch$ некоторых состояний связанных отношением   $\preceq$ на котором  $\preceq_*$  линейно. Глубина состояния $s \in T(M)$  это длина цепи ведущей из корня в $s$.


 \medskip

 {\bf Определение 1. } Пара $\langle T(M),  \preceq_*  \rangle$ называется
 фреймом ветвящегося времени с бинарным отношением временной достижимости  $\preceq_*$.

 \medskip

Далее, продолжая принятые обозначения, через $Sl_k(T(M))$ обозначаем множество всех состояний глубины  $k$ из $T(M))$  -- это $k$-й слой фрейма
$T(M))$; $S_k(T(M))$ это все состояния из $T(M))$,   глубины не выше $k$.
Введенное определение хорошо согласуется с интуицией о времени и далее мы специфицируем временную достижимость на восприятие агентов.
Ранее в статье  [11] в любой временной цепи выбирались фокальные временные состояния
делящие временные цепи на интервалы возможной временной достижимости для всех агентов.

Далее, развивая идею, [14,16], внутри интервалов агенты могли иметь интервалы потерянного времени и другие интересные черты многоагентного подхода. Но ограничения однородной ограниченности верхнего предела временной достижимости для всех агентов выглядело довольно искусственно. Хотя с другой стороны это отражало принятый взгляд на интервальную логику -- в любом состоянии время так сказать локально.  Этот подход  применения интервальной временной логики характерное для работ [13,14,15]. В данное работе мы сможем снять это ограничение.

Пусть $s$ некоторое состояние из $T(M)$. Из $s$ исходит множество полных временных цепей $A$
по $\preceq_*$   (т.е. просто последовательностей $A$ максимальной длины некоторых состояний, где соседние члены связаны отношением  $\preceq$). Обозначим множество всех таких полных цепей через $Ch(T(M))(s)$.

 Для любой полной временной цепи $A$ по $\preceq$  исходящий из временного состояния $s \in A$
 и $j \in J$, отношение временной достижимости
 \(R_s^j(A)\)
  из $s$ для агента $j$ в цепи  $A$ есть
  линейный прядок $\preceq_*$ порожденный конкатенацией отношения $\preceq$  на интервале состояний

  \[ [s, a_s(A)] := \{s\preceq s_1 \preceq  . . . \preceq s_{k-1} \preceq s_{k} = a_s(A) \}\]
  ведущих по $\preceq$ из $s$ в  некоторое выбранное зафиксированное состояние $a_s(A) \in A$   внутри цепи $A$  (в частности может быть $a_s(A) = s$).

Таким образом $R_s^j(A)$  свой собственный на каждом $s$ и для каждого $j$ и для каждой $A$.
Помимо этого накладываем естественное ограничение на согласованность отношения временной достижимости на
соприкасающихся разных цепях. А именно,

(i) если $s$  состояние из разных цепей $A_1$   и $A_2$ начинающихся с некоторого $s$ и $s \preceq_* a_s(A_1)$ и
$s \preceq_* a_s(A_2)$ и  $a_s(A_2) \not\in A_1$ и $b$ максимальное по $\preceq_*$ из $A_1$ входящее в
$A_2$ то   $b \preceq_* a_s(A_1)$. Неформально говоря это означает, что  линейные порядки локальной временной достижимости для одного агента те же до тех пор пока время не расщепилось.


(ii) Если $a R_a^j(A) b $  и $ b R_b^j(A) c, с \in A$ то  $a R_a^j(A) c $  - это так сказать свойство  локальной квазитранзитивности внутри самих временный цепей полной временной  достижимости для любого агента  $j$.

\medskip

{\bf Определение 2.}
{\it     Временной многоагентный фрейм это тройка
\[ F := \langle T(M), \{ R_x^j(A) \mid  x \in  T(M), j \in J, A\in Ch(T(M))(s_0) \},
  {\it Nxt}, \rangle, \mbox{ где },\]
   \[ \forall x,y \in T(M), \ x \  Nxt  \ y  \  \Leftrightarrow
   (\ x \preceq y \vee (\mbox{ $x$--$\preceq_*$-maximal $\& x=y $}). \] }

\medskip

Заметим что выше $\{ R_x^j(A) \mid  x \in  T(M), j \in J, A \}$ является множеством бинарных отношений временной достижимости.

Модель на временном многоагентном  фрейме $F$ задается путем введения означивания
 $V$ на $F$  для некоторого фиксированного множества пропозициональных переменных $p$, полагается
$V(p) \subseteq   T(M) $, и все состояния из $V(p)$  это все элементы из $F$ где $p$   считается истинным относительно означивания $V$. Это означивание распространяется на все формулы построенные из этих пропозициональных переменных следующим образом.

\medskip

{\bf Определение 3.} Для любого $a\in T(M)  $:

\[  \left(F,a\right) \Vdash_{V}  p  \ \Leftrightarrow \ \  p \in V(p); \]
\[ \left(F,a\right) \Vdash_{V}  \neg \varphi  \ \Leftrightarrow \ \  \left(F,a\right) \nVdash_{V_j}  \varphi;  \]
\[
\left(F,a\right)  \Vdash_{V} \left(\varphi\ \wedge \ \psi\right) \  \ \Leftrightarrow  \ \
(\left(F, a\right) \Vdash_{V} \varphi \right) \wedge \left(F,a\right) \Vdash_{V}  \psi\right);\]
\[
\left(F, a\right) \Vdash_{V} \left(\varphi \ \vee \ \psi\right) \  \ \Leftrightarrow  \ \
\left(F, a\right) \Vdash_{V} \varphi \right) \vee \left(F, a\right) \Vdash_{V}  \psi\right);\]
\[\left(F, a\right) \Vdash_{V} \left(\varphi \ \rightarrow \ \psi\right) \  \ \Leftrightarrow  \ \
\left(F, a\right) \nVdash_{V} \varphi \right) \vee \left(F, a\right) \Vdash_{V}  \psi\right);\]


Для формул $ \varphi {\bf U}_j \psi$  определение следующее:

\[\left(F,a\right) \Vdash_{V} \left(\varphi \ {\bf U}_j \ \psi\right) \  \Leftrightarrow  \
 (\exists  b \in T(M), \exists A\in Ch(T(M))(s_0) \left[
 \left(a R_a^{j}(A)  b\right)\wedge
\left(\left(F,b\right)\Vdash_{V} \psi\right) \ \& \]
\[\forall c (a \preceq_*  c \preceq_* b, c \in A,  c \neq b ) \ \ri \
\left( F,c\right)\Vdash_{V} \varphi \right]]), \]
\[
\left(F,a\right) \Vdash_{V} Next \ \varphi  \  \Leftrightarrow  \ \exists b \in T(M)\big[  \left(a \ \prec\  b \right) \ \& \ \left(F, b\right) \Vdash_{V} \varphi \big].\]

\medskip

Заметим что мы можем определить через введенные временные логические операции модальные операции специфицируемые для агентов. Например операция {\it возможно для $j$} может быть введена следующим образом:
\( \Diamond_j p := \top U_j p. \)
Операция необходимо для $j$ тогда выглядит так: $  \Box_j p := \neg \ U_j \neg p $.

\medskip

{\bf Определение 4}. {\it Временная степень $td(\varphi)$  любой формулы
$\varphi$, определяется индуктивно следующим образом.
Если  $\varphi$ является пропозициональной переменной то
$td(\varphi) := 0$. Если  $\varphi =     \varphi_1 \circ \varphi_2$ где $\circ$ является бинарной булевой логической операцией, то
 $td(\varphi) := max\{td(\varphi_1),td(\varphi_2)\}$;
если $\varphi =    \neg \varphi_1$ то $td(\varphi) := td(\varphi_1)$.
Если $\varphi =    Nxt \varphi_1$ то $td(\varphi) := td(\varphi_1) + 1$. Если
$\varphi =     \varphi_1 U_j \varphi_2$ то
$td(\varphi) := max\{td(\varphi_1),td(\varphi_2)\} +1 $.}

\medskip

Если некоторая формула имеет вид $\varphi_1 U_j \varphi_2$ или  $Nxt \varphi_1$ говорим что эта формула имеет главную временную связку. Для $s \in T(M)$, $s^\preceq :=  \{ a \mid s \preceq_* a, a \in T(M)\}$.
Для любой формулы $\varphi$ через $Sub(\varphi)$ обозначим множество всех подформул формулы $Sub(\varphi)$.

\medskip

{\bf Лемма 5.} {\it Пусть формула $\varphi$ имеющая $k$ подформул с главной временной связкой и $F$ некоторая модель с корнем $s$. Тогда существует подмодель $F_1$, получаемая из $F$  удалением некоторых полных временных цепей  из $s^\preceq \setminus \{s\}$ такая, что $s$ в $F_1$  имеет ветвление не более $k$ и выполняется
\[\forall \psi \in Sub(\varphi) [ (F,s)\Vdash_V \psi   \Leftrightarrow (F_1,s)\Vdash_V \psi  ]. \]
 }

\medskip

Доказательство.
Для  любой формулы $ \varphi_1 U_j\varphi_2 \in Sub(\varphi)$, если

\[(F,s)\Vdash_V \varphi_1 U_j \varphi_2   \ \ \mbox{ и   } \ \ (F,s)\nVdash_V   \varphi_2\]
выберем
\( Rt^s(\varphi_1 U_j\varphi_2 )\) --- некоторое состояние из второго слоя модели $F$ -- такое что $s \preceq Rt^s(\varphi_1 U_j \varphi_2)$ и

\[ (F,s)\Vdash_V \varphi_1 \ \& \  (F,Rt^s(\varphi_1 U_j \varphi_1 ) \Vdash_V \varphi_1 U_j \varphi_2. \]
Если  $ Nxt \varphi_1 \in Sub(\varphi)$ и
$(F,s)\Vdash_V Nxt \varphi_1$ выберем некоторое состояние $ Rt^s(Nxt \varphi_1) $ из $F$ такое что
$s Nxt Rt^s(Nxt \varphi_1)$ и
\( (Rt^s(Nxt \varphi_1),s)\Vdash_V \varphi_1\).
Теперь модернизируем модель $F$ удаляя все полные цепи начинающиеся с состояний отличных от $s$  и всех выбранных
\( Rt^s(\varphi_1 U \varphi_2 )\) и  $ Rt^s(Nxt \varphi_1) $ и обозначим оставшуюся модель через
$F_1$. Утверждаем что


\[\forall \psi \in Sub(\varphi) [ (F,s)\Vdash_V \psi   \Leftrightarrow (F_1,s)\Vdash_V \psi  . \]
}

Доказательство следует стандартным применением индукции по временной степени формул $\psi$
$\Box$.

\medskip

{\bf Лемма 6.} {\it Пусть формула $\varphi$ имеющая $k$ подформул с главной временной связкой и $F$ некоторая модель. Тогда для некоторой подмодели $F_1$, полученной из $F$  удалением некоторых полных временных цепей начинающихся с некоторых состояний
\[\forall \psi \in Sub(\varphi) [ (F,s)\Vdash_V \psi   \Leftrightarrow (F_1,s)\Vdash_V \psi  . \]
 }
где в $F_1$  любое состояние имеет ветвление не более $k$
\medskip

Доказательство: достаточно применить Лемму 5  двигаясь от корня по $ \preceq $ к непосредственным последователям.



\section{Проблема Выполнимости}


Напомним определение. Пусть дан некоторый класс моделей $K$ и некоторая формула  $\varphi$; формула  $\varphi$  называется выполнимой (в  $K$) если в некоторой модели из этого класса в некотором ее состоянии формула   $\varphi$  истинна. В нашем случае  класс $K$  моделей определен - это наши модели ветвящегося времени с разделенными отношениями временной достижимости агентов. Т. е. формула $\varphi$    выполнима если существует модель $M$  базирующаяся на некотором фрейме  $T(M)$   и имеющая означивание  $V$ такое, что
$\exists s\in T(M) [(T(M),s) \Vdash \varphi ] $ .
Выполнимость тесно связана с разрешимостью логики задаваемой некоторым классом моделей $K$. Логика $L(K)$  это множество всех формул которые истинны в любой модели на любом ее состоянии при всех возможных означиваниях истинности переменных.    Логика разрешима если существует алгоритм, проверяющий по любой данной формуле $\varphi$ верно ли  $\varphi \in L(K)$. Очевидно что $\varphi \in L(K)$  если и только если  $\neg\varphi$ не выполнима. И обратно   $\varphi$    выполнима если и только если  $  \neg\varphi$  \not\in L(K)$.


Таким образом, нам будет необходимо отыскать  алгоритм проверяющий
выполнимость формул на таких конечных моделей размер которых пока невозможно оценить.
Казалось бы наш класс определяющих моделей состоит только из конечных моделей и достаточно определить только размер опровергающей модели.
В теории неклассических логик обычно в таких случаях используется нечто вроде фильтрации или техники прореживания.
К сожалению здесь это прямо не работает из за операторов сорта $U_j$ - until. Дело в том что реализаторы формул $\varphi U_j  \psi$
влекут за собой цепи состояний ведущих в них -- и состояния этих цепей сохраняют истинность формул
$\varphi$ и такие состояния нельзя просто прореживать -- ибо логика ветвящегося времени -- и эти состояния могут требовать реализаторов в разных различных разных ветвящихся цепях. Поэтому нужно развить и применить более продвинутую технику.

Будем использовать сведение истинности формул к специальным правилам вывода в редуцированной форме которую мы ранее использовали в ряде работ [11,12,13].
Полезный эффект ее применения
состоит в том что в доказательствах  и конструкциях мы будем использовать только формулы в очень простой и регулярной форме где любая формула имеет временную степень не более 1. Кратко напомним базисные определения.
Правило \( {\bf r}:\) это выражение (инструкция ) \(\varphi_1( x_1, \dots ,
x_n), \dots ,\) \( \varphi_s( x_1, \dots , x_n) \ / \ {\psi(x_1, \dots , x_n)},
\) где все $\varphi_j( x_1, \dots ,
x_n),  \psi(x_1, \dots , x_n)$  это некоторые формулы построенные из некоторых переменных из списка
$x_1, \dots , x_n$.

В дальнейшем если не специфицированно точнее любая модель $M$  это либо модель из класса $K$  либо
конечная модель из Леммы 9.

\medskip

{\bf Определение 7.}
Правило
\( {\bf r}:= \varphi_1( x_1, \dots ,
x_n), \dots ,\) \( \varphi_s( x_1, \dots , x_n) \ / \ {\psi(x_1, \dots , x_n)},
\)
истинно на модели   $M$ если и только если

$$\textstyle{ [\forall a \left(\left({M,a}\right) \Vdash_{V} \bigwedge_{1\leq i \leq s}\varphi_i\right)]  \ \ \Rightarrow   \ \
 \left[ \forall a  \left(\left(M,a\right) \Vdash_{V_l} \psi\right)\right].}
 $$

 Если \(\forall a \left(\left({M,a}\right) \Vdash_{V}
\bigwedge_{1\leq i \leq s}\varphi_i\right) \) но
 \(\exists a \left(\left(M,a\right) \nVdash_{V} \psi\right)\),
мы говорим что ${\bf r}$ опровергнуто в  $M$ означиванием  $V$ и обозначаем от факт символом
 $ M \nVdash_{V} {\bf r}$.

\medskip

{\bf Лемма  8.}  Формула $\varphi$ выполнима на некоторой модели из  $K$ (или из классе конечных моделей из Леммы  9) если и только если правило  $ x \rightarrow x / \neg \varphi $
может быть опровергнуто на этой модели из $K$  (этого класса).

\medskip

Доказательство легко следует из определений.

\medskip
 Нам необходимо сведение правил вывода к нормальной форме.

\medskip

{\bf Определение 9.}
Говорим что правило ${\bf r}$ находится в нормальной редуцированной форме
если \( {\bf r}= \varepsilon / x_1\), где

\begin{eqnarray*}
\varepsilon &=&
 \bigvee_{1\leq j \leq p}
 \Big[ \bigwedge_{1\leq i \leq n}
 x_i^{t(j,i,0)} \wedge
\bigwedge_{1\leq i \leq n}
 \left(Nxt \ x_i\right)^{t(j,i, 1)} \wedge \\
 &&\phantom{\bigvee_{1\leq j \leq m}}\wedge
\bigwedge_{l \in [1,k], 1\leq i,k_1 \leq n }
\left(x_i U_l x_{k_1}\right)^{t(j,i,k_1,l,2)}\Big],
\end{eqnarray*}
%\bigwedge_{1\leq i \leq n}
% (\nn x_i)^{t(j,i,1)}
%({\bf \Diamond^+} x_i)^{t(j,i,1)}\wedge
%(\Diamond^- x_i)^{t(j,i,2)}  \wedge\]
%\[ ( \pp
%x_i)^{t(j,i,3)} \wedge
%(x_i \uu
%x_k)^{t(j,i,k,0)} \wedge (x_i  \uu_w x_k)^{t(j,i,k,1)} \wedge (x_i
%\uu_s x_k)^{t(j,i,k,2)} \wedge\]
%(\neg {\bf K}_q \neg x_i)^{t(j,i,q,1)} \wedge {\bf
%KnI}x_i^{t(j,i,3)} \wedge  (\mbox{U_J} x_i)^{t(j,i,4)}]), \] all $x_s$ are certain letters (variables),
 $t(j,i,0)$, $t(j,i,l,1)$, $t(j,i,k_1,l,2)$ $\in \{0,1\}$
 и для любой формулы  $\psi$ above
 $\psi^0 := \psi$, $\psi^1:= \neg \psi$.


\medskip

{\bf Определение 10. } Для любого правила ${\bf r }$, правило
${\bf r_{nf}}$  в редуцированной нормальной форме называется
 {\em редуцированной нормальной формой правила   ${\bf r }$} если и только если
\begin{itemize}
\item[(i)] ${\bf r_{nf}}$ содержит все переменные из ${\bf r }$ и может быть некоторые дополнительные;
\item[(ii)] Для любой модели $T(M)$,  правило
${\bf r }$ может быть опровергнуто на
$T(M)$ если и только если
${\bf r_{nf}}$  может быть опровергнуто на этой модели.
\end{itemize}


\medskip



{\bf Теорема 11.} \label{mt3} {\it Существует алгоритм  перестраивающий любое данное правило $\bf r$ в его нормальную редуцированную форму $\bf r_{nf}$ за (оно)-экспоненциальное время.
Переменные правила
$\bf r_{nf}$ это переменные из $\bf r$ и дополнительные переменные обозначающие все подформулы правила
 $\bf r$.}

\medskip

Редуцированные нормальные формы строимые по алгоритму заявленному в этой теореме  определены однозначно.
Далее, говоря о правилах в редуцированной нормальной форме мы всегда имеем ввиду только такие правила.
Доказательство этой моей теоремы известно с 1984, приведено с тех пор в ряде работ - см. например
доказательство Лемма 2 в [19] или аналогичного утверждения в [20].

\medskip


{\bf Лемма  12} \label{mlmm3} {\it Если некоторая формула $ \varphi$ выполнима и правило $\bf r_{nf}$ в редуцированной нормальной форме для правила $x \rightarrow x /\neg \varphi$  соответственно опровержимо в некоторой конечной модели базирующейся на фрейме
 $F $ с ветвлением не более числа подформул в $\varphi$, то
 $\bf r_{nf}$ опровержимо и $\varphi$ выполнима и на такой конечной модели размера вычислимого через размер правила
 $\bf r_{nf}$}$.

\medskip


\noindent{\sl Proof}. Пусть
\( {\bf r_{nf}}= \varepsilon / x_1\), где $\varepsilon = \bigvee_{1\leq j \leq m} \theta_j$,
\begin{eqnarray*}
\theta_j &=&
\Big[ \bigwedge_{1\leq i \leq n}
 x_i^{t(j,i,0)} \wedge
 \bigwedge_{1\leq i \leq n}
 \left(Nxt \ x_i\right)^{t(j,i,1)} \wedge
 \\
 &&
\phantom{\Big[}
\wedge
\bigwedge_{l \in [1,k], 1\leq i,k_1 \leq n }
\left(x_i U_l x_k\right)^{t(j,i,k_1,l,2)}   {\Big],
\end{eqnarray*}
и  $\bf r_{nf}$ опровержимо в некоторой модели $F$; очевидно можем считать что оно и сама формула $ \varphi$ опровержимы на ее    корне $s_0$.
Т.е.

\[(F, s_0) \Vdash \neg \varphi ;
(F, s_0) \Vdash \neg x_1 $; $\forall c , (F, c) \Vdash \varepsilon.\]


Итак мы можем считать что $F$ это конечное дерево  с корнем  $s_0$ состоящее из цепей с ветвлением ограниченным числом  подформул формулы $\varphi$ и c одинаковой длиной всех полных цепей исходящих из корня (хотя размер этой модели неизвестен и не имеет пока вычислимой верхней границы); и заключение правила - $x_1$ -- опровергается на корне $s_0$ и


\[  \forall a \in |M|, (M,a) \Vdash_V \bigvee_{1\leq j \leq m} \theta_j\]

Ввиду того что
\(  \forall a \in |M|, (M,a) \Vdash_V \bigvee_{1\leq j \leq m} \theta_j\) для любого
$a \in |M|$ существует единственное $\theta_j$ истинное на $a$ при $V$, обозначим его через
$\theta(a)$.

Зафиксируем любую произвольную максимальную полную цепь
 в этой модели исходящую из $s_0$:

\[ Ch(s_0) := \{ s_0  < \dots < s_m     \}. \]
и соответствующую последовательность

\[  Ch(s_0)^\theta := \{ \theta(s_0)  , \dots  , \theta(s_{m-1}), \theta(s_m)    \}. \]
Если формула $\theta(s_{m-1})$ как формула присутствует в этом списке  $Ch(s_0)^\theta$ еще раз -- выберем первое (наиболее раннее) ее вхождение в
 нашу последовательность - пусть это будет  $\theta(s_{m_k})$, т.е.

 \[\theta(s_{m_k}) = \theta(s_{m-1}) \ \
 \mbox {  и тогда  } \]


\[  (M,s_{m_k}) \Vdash_V \theta(s_{m_k})  \ \mbox{  и }
 (M,s_{m-1}) \Vdash_V \theta(s_{m_k}). \]
Преобразуем модель следующим образом -- удаляем все состояния цепи

\[ \{ s_{m_{k}} < \dots < s_{m-2}      \} \]
и все цепи восходящие из этих состояний $\{ s_{m_{k}} , \dots , s_{m-2},\}$ кроме самого состояния $s_{m-1}$ и его последователей.
Считаем что $s_{m_{k-1}} Next \ s_{m-1}$.
Теперь требуется переопределить отношения временной достижимости R_j^s(A)на элементах модифицируемой модели.

(a) Для состояний $s$ из $s_{m-1}^\preceq$ оставляем $R_j^s(A)$ прежними.

(b) Для  состояний $s$ из временной цепи ведущей в $s_{m_{k}}$ мы  расширяем $R_j^s(A)$ (временные интервалы достижимости) следующим образом:
для любого агента $j$ если ранее отношения $R_j^s(A)$ достигали состояния $s_{m_{k}}$,
то есть

\[ (s R_j^s(A)  s_{m_{k}}), \]
то мы склеиваем $R_j^s(A)$ с интервалами временной достижимости для $j$ из состояния
$s_{m-1}$ -- т.е. c $R_j^{s_{m-1}}(A)$.

Для остальных состояний мы не меняем отношения достижимости по времени для агентов $j$.
Обозначим модифицированную модель через $M_1$.

 \medskip

 {\bf Лемма 13.} {\it
  Модифицированная модель $M_1$  сохраняет истинность формул вида $x_1 U_j x_2$  и
 $Nxt \ x_i$ из посылки правила (и следовательно всех формул из посылки правила) той же что она и была на исходной модели.}

\medskip

  Доказательство. Действительно, пусть
 существуют формулы $x_1 U_j x_2$ такие что в исходной модели

\[ (M,a) \Vdash_V x_1 U_j x_2, \ \   a \preceq_* s_{m_{k-1} \]

и
\[ \exists b, (M,b) \Vdash_V x_2, s_{m_k} \preceq_* b  , a R_j^a(A)b \ \& \ \]
\[ \forall c (a \preceq^* c \preceq^* b, c \neq b )   [ (M,c) \Vdash_V x_1,
\ \mbox{   и } \ (M,c) \nVdash_V x_2 ]. \]


Тогда имеем

\[ (M,s_{m_k}) \Vdash_V x_1 U_j x_2, \mbox{ и   } \]

\[ (M,s_{m-1}) \Vdash_V x_1 U_j x_2, \]
и тогда
\[ (M_1,a) \Vdash_V x_1 U_j x_2 \]
так как (см. (b) выше) мы расширяли отношения временной достижимости из $a$ через $s_{m_k}$ и $s_{m-1}$.




  Остается проверить что ложность формул вида $x_1 U_j x_2$ тоже сохраняется.
 Для состояний не входящих в цепь

\[ \{ s_0  < \dots < s_{m_{k-1}}    \} \]
мы не меняли отношения временной достижимости и следовательно ложность формул указанного вида сохраняется. Пусть $s_0  \preceq_* \dots \preceq_* b \preceq_* \dots \preceq_* s_{m_{k-1}}$  и

\[ (M,b) \nVdash_V x_1 U_j x_2, \ \
\mbox { но  }
\ \  (M_1,b) \Vdash_V x_1 U_j x_2, \]

В этом случае

\[ (M_1,s_{m_{k-1}}}) \Vdash_V x_1 U_j x_2,
\ \ \mbox { и  } \ \
 (M_1,s_{m-1}) \Vdash_V x_1 U_j x_2, \]
и тогда
\[ (M,s_{m-1}) \Vdash_V x_1 U_j x_2. \]
Из  \(\theta(s_{m_k}) = \theta(s_{m-1})\) получаем
\[ (M,s_{m_k}) \Vdash_V x_1 U_j x_2 \ \ \mbox { и  }
\ \  (M,b) \Vdash_V x_1 U_j x_2 \]
-- противоречие. Случай формул вида  $Nxt \ x_i$ из посылки правила практически очевиден.
Лемма доказана.

\medskip

В силу этой леммы модель $M_1$  сохраняет  истинность формул вида $\theta(s_i)$ той же что она была и в исходной модели.
После этого рассматриваем $s_{m_{k}-1}$ как $s_{m-1}$ выше и также удаляем возможные дубликаты и продолжаем эту процедуру двигаясь по этой цепи к корню. В итоге через число шагов не более чем число формул $\theta_j$ в
$\bigvee_{1\leq j \leq m} \theta_j$, достигаем того что число состояний в рассматриваемой цепи не более чем $m$.

После этого берем другую максимальную цепь и выполняем такое же преобразование и так обрабатываем все максимальные цепи.

В силу того что исходная модель конечна преобразование завершится в конечное число шагов число которых мы пока прямо оценить не можем  (это зависит от числа возможных цепей максимальной длины в исходной модели которое исходно было неизвестно). Но вспомним что ветвление в исходной модели было ограниченно числом подформул формулы $\varphi$ и что наши преобразования не увеличивают размера возможных ветвлений получаем что полученная модель имеет ветвление не более $|| Sub(\varphi)||$ и что длина максимальных цепей в полученной модели не превышает числа формул $\theta_j $ в посылке правила, получаем что построенная модель конечна и имеет вычислимый максимальный возможный размер по размеру формулы $\varphi$. Лемма доказана.
 $\Box$.


\bigskip

Теперь, опираясь на доказанные леммы, получаем,  что проблема выполнимости разрешима.

\medskip

{\bf Теорема  14. }{\it Проблема выполнимости разрешима. }

\medskip

Доказательство. По лемме 6 достаточно проверить выполнимость формулы $\varphi$
в классе всех конечных моделей с ветвлением не выше $||Sub(\varphi)||$.
По Лемме 8  достаточно проверить опровержимость правила  $r(\varphi) := x \rightarrow x / $   на таких моделях. То Теореме 11 мы можем рассматривать редуцированную нормальную форму этого правила.
По Лемме  12 мы может рассматривать только конечные модели  размера вычислимого по
размеру правила $r(\varphi)$. $\Box$

\medskip




\section{Заключение}

Остались открытие интересные проблемы в  этой области. Во первых, случай с пробелами в восприятии времени агентами (Lacunas) в предложенной логике не решен. Расширение базисных моделей на возможные бесконечные также актуален и не решен. Помимо этого ветвящееся время всегда рассматривается в духе концепции что если время расщепилось однажды - то оно уже никогда не совмещается -- это допущение не слишком подтверждаемое практикой - к тому же -- интерпретационно --  вычислительные потоки сами расцепившись могут впоследствии и слиться. Этот случай все еще не изучен.
Вопрос о вычислении объективной истинности через суммированные значения истинности с  точки зрения агентов но уже специфицированные для каждых временных состояний -- также не разработан. Ну и проблематика построения эффективных аксиоматических систем и допустимых правил вывода также актуальна.


\bigskip

{\Large \sc Список литературы}

%\begin{thebibliography}{10}

\medskip

\begin{thebibliography}{90}

\medskip

[1] Gabbay D.M., Hodkinson I.M.
and Reynolds M.A.
  {\em ``Temporal
Logic'',} - { Mathematical
Foundations and Computational Aspects,}
vol. 1., Clarendon Press,
Oxford (1994).

\medskip

[2] Gabbay D.M., Hodkinson I.M.
 {\em ``An axiomatization of
the temporal logic with Until
and Since over the real numbers'',}
{Journal of Logic and Computation},
vol. 1, 229 -- 260 (1990),  229 -- 260.

\medskip

[3]
 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).



[4]
 Wooldridge M. and  Lomuscio A.
 {\em ``Multi-Agent VSK Logic'',}
 in: Proceedings of the Seventh European
 Workshop
 on Logics in Artificial Intelligence (JELIAI-2000), 2000,  Springer-Verlag, September 2000.

\medskip

[5]
Wooldridge. {\em ``An Automata-theoretic
approach to multi-agent planning'', }  in:
 Proceedings of the First European Workshop
 on Multi-agent Systems (EUMAS 2003), Oxford
 University, December 2003.

\medskip

[6]
 Wooldridge M., Huget M.P.,  Fisher M.,
 and Parsons S., ``Model Checking Multi-Agent
 Systems: The MABLE Language and Its Applications'',
 International Journal on Artificial Intelligence
 Tools, vol.15. no. 2, 195 -- 225 (2006).

\medskip



[7]
Belardinelli F. and Lomuscio A. {``Interactions
between Knowledge and Time in a First-Order
Logic for Multi-Agent Systems: Completeness Results'',}
 Journal of Artificial Intelligence Research,
 vol. 45,  1--45 (2012).


\medskip



[8] Emerson, E. A.; Halpern, J. Y. (1985). "Decision procedures and expressiveness in the temporal logic of branching time". Journal of Computer and System Sciences. 30 (1): 1–24. doi:10.1016/0022-0000(85)90001-7.

\medskip


[9] Clarke, E. M.; Emerson, E. A. & Sistla, A. P. (1986). "Automatic verification of finite-state concurrent systems using temporal logic specifications". ACM Transactions on Programming Languages and Systems. 8 (2): 244–263. doi:10.1145/5397.5399.

\medskip


[10]  J. Carmo and A. Sernadas. Branching vs linear logics yet a gain.
Formal Aspects of Computing, 2:24–59, 1990, 1170.

\medskip

[11] V.Rybakov,
Non-transitive linear temporal logic and logical knowledge operations
, J. of
Logic Comput., Oxford Press, 26
:3 (2016), 945–958. Zbl 1403.03028

\medskip


[12]
 V. Rybakov, ``Intransitive Temporal
 Multi-agency Logic, Knowledge and Uncertainty,
 Plausibility'', in:
International Symposium on Logical
Foundations of Computer Science,
Lecture Notes in Computer Science,
2016, pp. 364-375, vol.
 9537.


\medskip

[13]
V.V. Rybakov,
Nontransitive temporal multiagent logic, information and knowledge,
deciding algorithms
, Sib. Math. J.,
58
:5 (2017), 875–886. Zbl 1420.03060

\medskip


[14]
V. Rybakov,
Multiagent temporal logics with multivaluations
, Sib. Math. J.,
59
:4 (2018),
710–720. Zbl 06976648

\medskip

[15]
V.  Rybakov,
Linear Temporal Logic with Non-transitive Time, Algorithms for
Decidability and Verification of Admissibility
, in
Outstanding Contributions to Logic
,
Springer, 2018, 219–243. Zbl 1429.03074

\medskip

[16]
V. Rybakov,
Temporal multi-valued logic with lost worlds in the past
, Sib. Electron.
Math. Izv.,
15
(2018), 436–449. Zbl 06931667
[25]

\medskip

[17]
V. Rybakov,
Branching time agents’ logic, satisfiability problem by rules in reduced
form
, Sib. Electron. Math. Izv.,
16
(2019), 1158–1170. Zbl 07122035

\medskip


[18] Rybakov V. V.
Temporal logic with accessibility temporal relations generated by time states themselves,
Sib. Electron. Math. Izv., 17, (2020), pp. 923-932.
 10.33048/semi.2020.17.068

\medskip

[19] S. Babenyshev, V. Rybakov,
Linear Temporal Logic LTL: Basis for Admissible Rules
, Journal
of Logic and Computation, Oxford Press,
21
:2 (2011), 157–177. Zbl 1233.03026

\medskip

[20]
V.V. Rybakov,
Logical Consecutions in Discrete Linear Temporal Logic
, J. of Symbolic
Logic,
70
:4 (2005), 1137–1149. Zbl 1110.03010

begin{thebibliography}{90}

%\end{thebibliography}

\end{document}

