Области практического использования средств автоматического доказательства теорем

Средства автоматического доказательства теорем позволили получить новейшие математические результаты. Программа SAM (Semi-Automated Mathematics) была первой программой, с помощью которой удалось доказать одну из лемм в теории решеток [602]. Кроме того, программа Aura позволила найти ответ на многие открытые вопросы в нескольких областях математики [1621]. Программа автоматического доказательства теорем Бойера-Мура [165] применялась и дорабатывалась в течение многих лет, и ею воспользовался Натараджан Шанкар для получения первого полностью строгого формального доказательства теоремы Гёделя о неполноте [1393]. Одним из самых строгих средств автоматического доказательства теорем является программа Otter; она использовалась для решения некоторых открытых задач в области комбинаторной логики. Наиболее известные из них касаются алгебры Роб-бинса. В 1933 году Герберт Роббинс предложил простое множество аксиом, которые, на первый взгляд, могли служить для определения булевой алгебры, но ни одного доказательства этой гипотезы найти не удавалось (несмотря на напряженную работу нескольких выдающихся математиков, включая самого Альфреда Тарского). Наконец, 10 октября 1996 года после восьми дней вычислений программа EQP (одна из версий программы Otter) нашла такое доказательство [1019].

Средства автоматического доказательства теорем могут также применяться для решения задач, связанных с проверкой и синтезом как аппаратных, так и программных средств, поскольку для обеих этих проблемных областей могут быть предусмотрены правильные варианты аксиоматизации. Поэтому исследования доказательства теорем проводятся не только в искусственном интеллекте, но и в таких областях, как проектирование аппаратных средств, языки программирования и разработка программного обеспечения. В случае программного обеспечения аксиомы определяют свойства каждого синтаксического элемента языка программирования. (Процесс формирования рассуждений о программах полностью аналогичен процессу формирования рассуждений о действиях в ситуационном исчислении.) Программный алгоритм проверяется путем демонстрации того, что его выходы соответствуют спецификациям для всех входов. Таким образом были проверены алгоритм шифрования RSA с открытым ключом и алгоритм согласования строк Бойера-Мура [166]. В случае аппаратного обеспечения аксиомы описывают способы взаимодействия сигналов и элементов схемы (один из примеров приведен в главе 8). Программой Aura [1610] был проверен проект 16-битового сумматора. Системы формирования логических рассуждений, предназначенные специально для проверки аппаратных средств, оказались способными проверять целые процессоры, включая свойства синхронизации этих процессоров [1455].