Циклические выводы для логики доказуемости Гёделя–Лёба

В статье рассматривается исчисление секвенций для логики доказуемости $\mathsf{GL}$, доказуемость в котором основана на понятии циклического вывода. В отличие от обычных выводов, циклический вывод можно представлять себе не как дерево, но как граф, содержащий циклы. Используя данное понятие, мы даем синтаксическое доказательство интерполяционного свойства Линдона для логики $\mathsf{GL}$.
Библиография: 18 названий.