Adaptive human–machine theorem proving system

В данной работе представлен новый подход к построению человеко-машинных систем доказательства теорем. Системы объединяют возможности машинного обучения, экспертные знания человека и строгий логический контроль для эффективного построения и верификации доказательств. Новизна подхода заключается в его открытости: в руки пользователя дается инструмент построения таких систем. С помощью него пользователь может создавать системы доказательства теорем, выбирая уже имеющиеся стратегии построения логического вывода или добавляя новые в соответствии с предоставленными интерфейсами или соглашениями о связях. Строящиеся системы имеют существенный человеко-машинный адаптивный характер. При их работе строится и обучается метастратегия на основе исходных элементов имеющихся стратегий. Система разработана как универсальная основа для управления различными стратегиями, с предоставлением базовой архитектуры и библиотеки стратегий с возможностью добавления новых. При обучении также накапливается и обучается система структурных характеристик, на основе которых принимается решение об использовании того или иного элемента стратегий на очередном шаге. Изложение ведется для секвенциального исчисления минимальной позитивной логики предикатов как наиболее подходящей для дедуктивного синтеза программ и алгоритмов, для чего и предполагается использовать данный подход.