Тип публикации: статья из журнала
Год издания: 2022
Идентификатор DOI: 10.33048/alglog.2022.61.505
Ключевые слова: temporal logics, multi-agent logics, Admissible inference rules, unification problem, solving algorithms, временные логики, мультиагентные логики, допустимые правила вывода, проблема унификации, разрешающие алгоритмы
Аннотация: Рассматриваются временные многоагентные логики, использующие новое трактование времени для индивидуальных агентов. Предполагается, что в любом временном состоянии любой агент в некотором смысле сам порождает будущее время, доступное ему для анализа, т. е. участок этого времени зависит как от данного стартового временного состояния,Показать полностьютак и от агента. Также предполагается, что любой агент может обладать участками забытого (потерянного) времени. Исследуются проблемы унификации и проблемы алгоритмического распознавания допустимых правил вывода. Алгоритмическое решение проблемы унификации состоит в нахождении конечного вычислимого множества формул, являющегося полным множеством унификаторов. Здесь применяется техника проективных формул, предложенная С. Гиларди. Доказывается, что каждая унифицируемая формула является проективной и строится алгоритм, конструирующий её проективный унификатор. Тем самым даётся решение проблемы унификации. Применяя этот результат, находится решение проблемы алгоритмического распознавания допустимых правил вывода. We study temporal multi-agent logics using a new approach to defining time for individual agents. It is assumed that in any time state each agent (in a sense) generates its own future time, which will only be available for analysis in the future. That is, the defined time interval depends both on the agent and on the initial state where the agent starts to act. It is also assumed that the agent may have intervals of forgotten (lost) time. We investigate problems of unification and problems of computable recognizing admissible inference rules. An algorithm is found for solving these problems based on the construction of a finite computable set of formulas which is a complete set of unifiers. We use the technique of projective formulas developed by S. Ghilardi. It is proved that any unifiable formula is in fact projective and an algorithm is constructed which creates its projective unifier. Thereby we solve the unification problem, and based at this, find the solution to the open problem of computable recognizing admissible inference rules.
Журнал: Алгебра и логика
Выпуск журнала: Т. 61, № 5
Номера страниц: 600-618
ISSN журнала: 03739252
Место издания: Новосибирск
Издатель: Новосибирский региональный фонд "Сибирский фонд алгебры и логики"