Программное обеспечение вычислительных, телекоммуникационных и управляющих систем

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

В. А. Павлов

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

Аннотация: Изложены результаты исследования, посвящëнного применению обратного метода Маслова для автоматизации логического вывода в интуиционистских логических исчислениях. Подробно рассмотрены адаптированные стратегии поиска вывода для интуиционистских исчислений обратного метода, а также новые стратегии, позволяющие ограничить возникающие переборы и уменьшить размер пространства поиска вывода. Также описаны детали реализации разработанной автором компьютерной программы WhaleProver, использующей обратный метод для логического вывода в интуиционистской логике первого порядка. Приведены результаты экспериментального сравнения предложенных стратегий друг с другом и новые результаты сравнения программы WhaleProver с существующими аналогами. Программа не уступает в эффективности лучшим из существующих аналогов (ileanCoP, Imogen) и даже позволяет решить новые задачи из библиотеки ILTP. Таким образом, на практике подтверждается, что программная реализация обратного метода может быть не менее эффективной, чем реализации других методов автоматического логического вывода (в частности, табличных методов).

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

УДК: 004.832.32

DOI: 10.18721/JCSTCS.10104