Ограничение сложности термов в выходах и разрешимые фрагменты исчисления предикатов
Представление доказательств раскрашенными графами и гипотеза Хадвигера
Применение изограмм в поиске вывода
Распространение обратного метода на аксиоматические теории с равенством
Семантически универсальные классы моделей.
Три способа выявления несущественных формул в секвенциях
Финитный подход к задаче оптимизации алгоритмов установления выводимости