Исправления к сборникам "Исследования по конструктивной математике и математической логике". II (1968) и III (1969)
Машинный алгорифм установления выводимости на основе обратного метода
Метод синтеза условий выводимости хорновских и некоторых других формул.
О метаматематическом подходе к доказательству теорем дискретной математики
О поиске вывода в исчислениях общего типа
О распознавании тавтологичности пропозициональных формул
О сложности линейных выводов в методе резолюций
Об одном классе стратегий, применяемых при установлении доказуемости методом резолюций
Одна схема доказательств в дискретной математике
Применение изограмм в поиске вывода
Распространение обратного метода на аксиоматические теории с равенством
Распространение обратного метода на исчисление с равенством
Связь между тактиками обратного метода и метода резолюций
Стратегия дефакторизации в методе резолюций
Стратегия упорядочивания дизъюнктов в методе резолюций
Тактики поиска вывода, основанные на унификации порядка членов в благоприятном наборе
Финитный подход к задаче оптимизации алгоритмов установления выводимости