Сибирский федеральный университет

Тип публикации: статья из журнала

Год издания: 2022

Идентификатор DOI: 10.33048/smzh.2022.63.417

Ключевые слова: temporal logic, Multi-agent logic, satisfiability problem, deciding algorithm, временные логики, многоагентные логики, проблема выполнимости, разрешающие алгоритмы

Аннотация: Изучается временная многоагентная логика с различными индивидуальными для каждого агента участками потерянного времени. Логика базируется на фермах с основными базисными множествами на всех натуральных числах $N$ как временных состояниях, где каждый агент $j$ может иметь собственные множества $X_j$ недоступных (потерянных, забытых) состояний времени ($\forall j\in J$, $X_j\subset N$). Основными математическими задачами исследования являются проблемы унификации и проблема алгоритмического распознавания допустимых правил вывода. Решение проблемы унификации состоит в нахождении конечного вычислимого множества формул, являющегося полным множеством унификаторов. Эта задача решается с применением техники проективных формул, предложенной Сильвио Гиларди. Доказано, что каждая унифицируемая в этой логике формула проективна, и построен алгоритм, конструирующий ее проективный унификатор. Тем самым решена проблема унификации. Это позволяет решить открытую проблему алгоритмического распознавания допустимых правил. Статья завершается введением обобщения определения проективных формул - слабо проективных формул, и простым примером его применения. Under study is the temporal multiagent logic with different intervals of lost time which are individual for each of the agents. The logic bases on the frames with principal basic sets on all naturals $N$ as temporal states, where each agent $j$ can have their own proper sets $X_j$ of inaccessible (lost, forgotten) temporal states ($X_j\subset N$ for all $j\in J$). The unification problem and the problem of the algorithmic recognition of admissible inference rules are the main mathematical problems of the paper. The solution of the unification problem consists in finding a finite computable set of formulas which is a complete set of unifiers. The problem is solved by the Ghilardi technique of projective formulas. We prove that every formula unifiable in this logic is projective and provide some algorithm constructing its projective unifier, which solves the unification problem. This makes it possible to solve the open problem of the algorithmic recognition of admissible rules. The article ends with some generalization of the definition of projective formulas -weakly projective formulas - and exhibits an easy example of their application.

Журнал: Сибирский математический журнал

Выпуск журнала: Т.63, №4

Номера страниц: 924-934

ISSN журнала: 00374474

Место издания: Новосибирск

Издатель: Сибирское отделение РАН, Институт математики им. С.Л. Соболева СО РАН

• Рыбаков Владимир Владимирович (Национальный исследовательский университет «Высшая школа экономики»)

• Ядро РИНЦ (eLIBRARY.RU)