On the unification problem for $\mathrm{GLP}$

Мы показываем, что полимодальная логика доказуемости GLP, сформулированная в языке по крайней мере с двумя модальностями и одной переменной, имеет нулевой унификационный тип. В частности, мы доказываем, что формула $[1]p$ не имеет максимальных унификаторов, и предъявляем для нее бесконечное полное множество унификаторов. Далее, мы обсуждаем алгоритмическую проблему унифицируемости данной формулы в GLP, и отмечаем, что эта проблема имеет положительное решение. Наконец, мы рассматриваем арифметические аналоги проблем унификации и допустимости правил вывода для логики GLP и формулируем несколько открытых вопросов.