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

В классической работе 1938 года Морс и Хедлунд доказали, что всякое непериодическое бесконечное слово содержит как минимум n+1 подслово длины n. Более того, бесконечное слово содержит ровно n+1 подслово для каждой длины n, если и только если оно бинарное, непериодическое и сбалансированное, т.е. является словом Штурма. В докладе мы рассмотрим обобщение понятия сложности слов через действия групп и обсудим обобщения теоремы Морса и Хедлунда.