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

This paper contains the results of the research related to Maslov's inverse method and its application to first-order intuitionistic logic. Several proof search strategies for the inverse-method intuitionistic calculus, which allow reducing the proof search space and avoiding redundant inferences, are proposed and explained in detail. Some strategies are new, others are adapted variants of the existing strategies for classical logic. This article includes a detailed description of the automated theorem-proving system WhaleProver for first-order intuitionistic logic, which is based on the inverse method.

Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Сер.: Информатика. Телекоммуникации. Управление = St. Petersburg state polytechnical university journal. Computer science. Telecommunications and control systems: научное издание. Т. 10, № 1. — Электрон. текстовые дан. (1 файл : 8,24 Мб). — Санкт-Петербург: Изд-во Политехн. ун-та, 2017. — Загл. с титул. экрана. — Электронная версия печатной публикации. — Свободный доступ из сети Интернет (чтение, печать, копирование). — Текстовый документ. — Adobe Acrobat Reader 7.0. — <URL:http://elib.spbstu.ru/dl/2/j17-341.pdf>.