Статья посвящена обратному методу Маслова, который подходит для автоматизации доказательств в различных логических исчислениях: логика высказываний, классическая логика первого порядка, интуиционистская логика, модальные логики и т. д. Приведен обзор основных публикаций по обратному методу, рассмотрено разработанное авторами исчисление обратного метода для интуиционистской логики первого порядка. Предложены адаптированные и оригинальные стратегии оптимизации для этого исчисления. Рассмотрены алгоритм логического вывода в полученном исчислении и разработанная на его основе программа автоматического доказательства теорем WhaleProver.

We discuss the inverse method of automated theorem-proving that was invented by S. Maslov. The inverse method can be applied to various logics: propositional logic, first-order logic, modal logics, intuitionistic logic, etc. In the current article, we present an overview of the key publications on the inverse method, describe in detail an inverse method calculus for first-order intuitionistic logic. We propose adapted as well as original optimizing strategies for the developed calculus. We discuss a proof search algorithm for the proposed calculus and our program implementation named WhaleProver.

Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Сер.: Информатика. Телекоммуникации. Управление = St. Petersburg state polytechnical university journal. Computer science. Telecommunications and control systems: научное издание. — Санкт-Петербург: ПОЛИТЕХ-ПРЕСС, 2008-. № 6 (234). — Электрон. текстовые дан. (1 файл : 4,93 МБ). — Санкт-Петербург: Изд-во Политехн. ун-та, 2015. — Электронная версия печатной публикации. — Загл. с титул. экрана. — Свободный доступ из сети Интернет (чтение, печать, копирование). — Текстовый файл. — Adobe Acrobat Reader 7.0. — <URL:http://elib.spbstu.ru/dl/2/j16-148.pdf>.