Специальные случаи интерполяционной теоремы для классического исчисления предикатов

В статье доказываются специальные случаи интерполяционной теоремы для классического исчисления предикатов без функциональных символов и равенства. Накладывая ограничения на интерполируемые формулы, можно доказать существование интерполянта особого вида: универсального, экзистенциального, хорновского и универсального хорновского. Наиболее интересен случай универсального хорновского интерполянта: аксиомы многих алгебраических систем задаются универсальными хорновскими формулами. Результаты, полученные в данной работе, могут быть полезны как с точки зрения теории доказательств, так и в приложениях, например, при решении задач искусственного интеллекта и разработке языков логического программирования. Статья написана в духе теории доказательств, основным инструментом для решения задачи служат секвенциальные исчисления и такие техники преобразования выводов, как обращение применений правил вывода, перестановка применений правил по С. К. Клини и прополка по В. П. Оревкову.
Статья состоит из введения, разбитой на 3 параграфа основной части и заключения. Введение содержит краткий исторический обзор и обсуждение актуальности работы. В первом параграфе основной части вводятся необходимые определения и формулируется главный результат. Второй параграф посвящён описанию построенного В. П. Оревковым секвенциального исчисления KGL. Третий отведён доказательству основной теоремы. Заключение содержит обсуждение полученных результатов и краткий обзор перспектив дальнейшей работы.