Исследовательская группа

Лаборатория языковых инструментов

Автоматическое доказательство теорем и обратный метод Маслова

December 19

Будет сделан обзор современных систем автоматического доказательства теорем и областей их применения, а также будут изложены результаты исследования, посвящённого применению обратного метода Маслова для автоматизации доказательств в интуиционистской логике первого порядка. Для информатики наиболее привлекательной особенностью этой логики является возможность извлечь алгоритм построения объекта с требуемыми свойствами из интуиционистского доказательства теоремы о существовании такого объекта.

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

Докладчик: Владимир Павлов, СПбПУ им. Петра Великого.

Материалы