Диссертация посвящена разработке методов эффективного поиска логического вывода в исчислении позитивно–образованных формул и реализации этих методов в форме программной системы автоматического доказательства теорем (АДТ). Программная система протестирована на наборе задач из библиотеки TPTP (www.tptp.org), проведено сравнение с иными системами АДТ.