Динамические временные операции в мультиагентных логиках

Рассматриваются временные многоагентные логики, использующие новое трактование времени для индивидуальных агентов. Предполагается, что в любом временном состоянии любой агент в некотором смысле сам порождает будущее время, доступное ему для анализа, т. е. участок этого времени зависит как от данного стартового временного состояния, так и от агента. Также предполагается, что любой агент может обладать участками забытого (потерянного) времени. Исследуются проблемы унификации и проблемы алгоритмического распознавания допустимых правил вывода. Алгоритмическое решение проблемы унификации состоит в нахождении конечного вычислимого множества формул, являющегося полным множеством унификаторов. Здесь применяется техника проективных формул, предложенная С. Гиларди. Доказывается, что каждая унифицируемая формула является проективной и строится алгоритм, конструирующий её проективный унификатор. Тем самым даётся решение проблемы унификации. Применяя этот результат, находится решение проблемы алгоритмического распознавания допустимых правил вывода.