Тип публикации: статья из журнала
Год издания: 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. (Плеадес Паблишинг, Лтд)