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

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

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

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

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

Аннотация: Under study is the temporal multiagent logic with different intervals of lost timewhich are individual for each of the agents.The logic bases on the frames with principal basicsets on all naturals $ N $ as temporal states, where each agent $ j $ can have theirown 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 arethe main mathematical problems of the paper.The solutionof the unification problem consists in finding a finite computable set of formulaswhich is a complete set of unifiers. The problem is solved by the Ghilardi techniqueof projective formulas. We prove that every formulaunifiable in this logic is projective and providesome algorithm constructing its projective unifier, which solves the unification problem. This makes it possibleto solve the open problem of the algorithmic recognition of admissible rules.The article ends with some generalization of the definitionof projective formulas—weakly projective formulas—and exhibits an easy exampleof their application. © 2022, Pleiades Publishing, Ltd.

Журнал: Siberian Mathematical Journal

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

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

ISSN журнала: 00374466

Издатель: Pleiades journals

• Rybakov V.V. (Institute of Mathematics and Informatics, Siberian Federal University, Krasnoyarsk, Russian Federation, A.P. Ershov Institute of Informatics Systems, Novosibirsk, Russian Federation, National Research University Higher School of Economics, Moscow, Russian Federation)

• Scopus