Рассматривается применение обратного метода Маслова для автоматического логического вывода в интуиционистской логике первого порядка. На данный момент существует немного программных реализаций обратного метода для этой логики, при этом остаётся пробел между теоретическими достижениями и их внедрением на практике.
Разработано новое исчисление обратного метода для интуиционистской логики первого порядка и стратегии логического вывода для этого исчисления.
Разработан алгоритм логического вывода с возможностью комбинирования стратегий, применимый к предложенному исчислению и к другим исчислениям обратного метода. На основе алгоритма разработана программа автоматического логического вывода WhaleProver.
Проведено экспериментальное сравнение используемых стратегий по ряду критериев, выявлена оптимальная комбинация стратегий.
Программа WhaleProver апробирована на обширной библиотеке задач ILTP версии 1.1.2. Всего программа решила 810 задач, что сопоставимо с результатами лучших аналогов. Решён ряд новых задач. Программу можно использовать для обучения или интегрировать в существующие системы искусственного интеллекта.