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

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

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

Идентификатор DOI: 10.1134/s0037446622040176

Ключевые слова: temporal logic, multiagent logic, satisfiability problem, deciding algorithm

Аннотация: 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 as temporal states, where each agent can have their own proper sets of inaccessible (lost, forgotten) temporal states ( for all ). 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.

Журнал: Siberian Mathematical Journal

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

Номера страниц: 769-776

ISSN журнала: 00374466

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

Издатель: Pleiades Publishing, Ltd. (Плеадес Паблишинг, Лтд)

• Rybakov V.V. (National Research University Higher School of Economics)

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