Projective formulas and unification in linear discrete temporal multi-agent logics

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