Аннотация:Данная статья продолжает наше исследование проблемы унифицируемости в многоагентных логиках. Основываясь на подходе к унификационной проблеме через проективные формулы, предложенном В. Рыбаковым и S. Ghilardi, в этой работе мы рассматриваем некоторые линейные дискретные временные логики с агентными отношениями. Мы доказываем проективность любой унифицируемой формулы в этих логиках и даем алгоритм построения наиболее общего унификатора.
Ключевые слова:унификация, модальная временная логика, пассивные правила вывода, проективные формулы, агентные отношения, Институт математики и фундаментальной информатики, ИМиФИ, сфу