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