Тип публикации: статья из журнала
Год издания: 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 statПоказать полностьюes($ 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