Интеллектуальные системы и технологии

Экспериментальная программа для доказательства теорем интуиционистской логики обратным методом Маслова

В. А. Павлов, B. Г. Пак

Институт компьютерных наук и технологий Санкт-Петербургского политехнического университета Петра Великого

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

Ключевые слова: автоматическое доказательство теорем, логический вывод, обратный метод, метод Маслова, интуиционистская логика.

УДК: 004.832.32

DOI: 10.5862/JCSTCS.234.7