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

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