Автоматическое доказательство теорем - Automated theorem proving

Автоматическое доказательство теорем (также известен как АТФ или же автоматический вычет) является подполем автоматическое рассуждение и математическая логика имея дело с доказательством математические теоремы к компьютерные программы. Автоматическое рассуждение математическое доказательство был основным стимулом для развития Информатика.

Логические основы

Хотя корни формализованных логика вернуться к Аристотель, конец 19 - начало 20 вв. ознаменовались развитием современной логики и формализованной математики. Фреге с Begriffsschrift (1879) представил как полную пропозициональное исчисление и что по сути современно логика предикатов.[1] Его Основы арифметики, опубликовано 1884 г.,[2] выразил (части) математики в формальной логике. Этот подход был продолжен Рассел и Уайтхед в их влиятельных Principia Mathematica, впервые опубликовано в 1910–1913 гг.,[3] и с исправленным вторым изданием в 1927 году.[4] Рассел и Уайтхед считали, что они могут вывести всю математическую истину, используя аксиомы и правила вывода формальной логики, в принципе открывая процесс для автоматизации. В 1920 г. Торальф Сколем упростил предыдущий результат Леопольд Левенхайм, ведущий к Теорема Левенгейма – Сколема а в 1930 году к понятию Вселенная Herbrand и Интерпретация Herbrand что допускало (не) выполнимость формул первого порядка (и, следовательно, срок действия теоремы) сводится к (потенциально бесконечному множеству) проблемам пропозициональной выполнимости.[5]

В 1929 г. Mojżesz Presburger показал, что теория натуральные числа с добавлением и равенством (теперь называется Арифметика пресбургера в его честь) разрешимый и дал алгоритм, который мог определить, было ли данное предложение на языке истинным или ложным.[6][7]Однако вскоре после этого положительного результата Курт Гёдель опубликовано О формально неразрешимых предложениях Principia Mathematica и родственных систем (1931), показывающий, что в любой достаточно сильной аксиоматической системе есть истинные утверждения, которые нельзя доказать в системе. Эта тема получила дальнейшее развитие в 1930-х годах. Церковь Алонсо и Алан Тьюринг, который, с одной стороны, дал два независимых, но эквивалентных определения вычислимость, а с другой - конкретные примеры неразрешимых вопросов.

Первые реализации

Вскоре после Вторая Мировая Война стали доступны первые компьютеры общего назначения. В 1954 г. Мартин Дэвис запрограммированный алгоритм Пресбургера для ДЖОННИАК ламповый компьютер в Принстонский институт перспективных исследований. По словам Дэвиса, «его большим триумфом было доказательство того, что сумма двух четных чисел является четной».[7][8] Более амбициозным был Логическая Теория Машины в 1956 году система вычета для логика высказываний из Principia Mathematica, разработан Аллен Ньюэлл, Герберт А. Саймон и Дж. К. Шоу. Также работающая на JOHNNIAC, машина логической теории построила доказательства на основе небольшого набора пропозициональных аксиом и трех правил дедукции: modus ponens, (пропозициональная) подстановка переменных и замена формул по их определению. Система использовала эвристическое руководство и сумела доказать 38 из первых 52 теорем Начала.[7]

«Эвристический» подход Логической Теоретической Машины пытался подражать человеческим математикам и не мог гарантировать, что доказательство может быть найдено для каждой действительной теоремы даже в принципе. Напротив, другие, более систематические алгоритмы, достигнутые, по крайней мере теоретически, полнота для логики первого порядка. Первоначальные подходы основывались на результатах Хербранда и Сколема для преобразования формулы первого порядка в последовательно увеличивающиеся наборы пропозициональные формулы путем создания экземпляров переменных с терминами из Вселенная Herbrand. Затем пропозициональные формулы могут быть проверены на неудовлетворительность с помощью ряда методов. Программа Гилмора использовала преобразование в дизъюнктивная нормальная форма, форма, в которой выполнимость формулы очевидна.[7][9]

Разрешимость проблемы

В зависимости от лежащей в основе логики проблема определения действительности формулы варьируется от тривиальной до невозможной. Для частого случая логика высказываний, проблема разрешима, но совместно NP-полный, и, следовательно, считается, что для общих задач доказательства существуют только алгоритмы с экспоненциальным временем. Для исчисление предикатов первого порядка, Теорема Гёделя о полноте утверждает, что теоремы (доказуемые утверждения) в точности логически верны правильные формулы, поэтому определение действительных формул рекурсивно перечислимый: при неограниченных ресурсах любая действительная формула в конечном итоге может быть доказана. Тем не мение, инвалид формулы (те, которые нет вытекает из данной теории), не всегда может быть распознан.

Сказанное выше относится к теориям первого порядка, таким как Арифметика Пеано. Однако для конкретной модели, которая может быть описана теорией первого порядка, некоторые утверждения могут быть верными, но неразрешимыми в теории, используемой для описания модели. Например, по Теорема Гёделя о неполноте, мы знаем, что любая теория, собственные аксиомы которой верны для натуральных чисел, не может доказать, что все утверждения первого порядка верны для натуральных чисел, даже если список собственных аксиом может быть бесконечным. Отсюда следует, что автоматическое средство доказательства теорем не сможет завершить поиск доказательства именно тогда, когда исследуемое утверждение неразрешимо в используемой теории, даже если оно истинно в интересующей модели. Несмотря на этот теоретический предел, на практике средства доказательства теорем могут решать множество сложных задач, даже в моделях, которые не полностью описываются какой-либо теорией первого порядка (например, целые числа).

Связанные проблемы

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

Поскольку доказательства, генерируемые автоматическими средствами доказательства теорем, обычно очень велики, проблема стойкое сжатие имеет решающее значение, и были разработаны различные методы, направленные на то, чтобы сделать результат проверки меньше и, следовательно, более легким для понимания и проверки.

Помощники доказательства требовать, чтобы пользователь-человек давал подсказки системе. В зависимости от степени автоматизации, доказывающая сторона может быть по существу сведена к проверке доказательства, при этом пользователь предоставляет доказательство формальным образом, или важные задачи доказательства могут выполняться автоматически. Интерактивные средства доказательства используются для множества задач, но даже полностью автоматические системы доказали ряд интересных и трудных теорем, включая по крайней мере одну, которая долгое время ускользала от математиков, а именно: Гипотеза Роббинса.[10][11] Однако эти успехи случаются нерегулярно, и для решения сложных проблем обычно требуется опытный пользователь.

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

Существуют гибридные системы доказательства теорем, в которых проверка модели используется в качестве правила вывода. Есть также программы, которые были написаны для доказательства конкретной теоремы с (обычно неформальным) доказательством того, что если программа завершается с определенным результатом, то теорема верна. Хорошим примером этого было машинное доказательство теорема четырех цветов, которое было очень спорным как первое заявленное математическое доказательство, которое было практически невозможно проверить людьми из-за огромного размера вычислений программы (такие доказательства называются не подлежащие обзору доказательства ). Другой пример программного доказательства - тот, который показывает, что игра Подключите четыре всегда может быть выигран первым игроком.

Промышленное использование

Коммерческое использование автоматического доказательства теорем в основном сосредоточено в конструкция интегральной схемы и проверка. Поскольку Ошибка Pentium FDIV, сложный единицы с плавающей запятой современных микропроцессоров были разработаны с особой тщательностью. AMD, Intel и другие используют автоматическое доказательство теорем, чтобы убедиться, что деление и другие операции правильно реализованы в их процессорах.

Доказательство теорем первого порядка

В конце 1960-х годов агентства, финансирующие исследования в области автоматизированной дедукции, начали подчеркивать необходимость практического применения. Одним из первых плодотворных направлений было проверка программы при этом средства доказательства теорем первого порядка применялись к проблеме проверки правильности компьютерных программ на таких языках, как Паскаль, Ада и т. д. Среди первых систем проверки программ был известен Стэнфордский верификатор Паскаля, разработанный Дэвид Лакхэм в Стэндфордский Университет. Это было основано на Стэнфордском модуле доказательства разрешающей способности, также разработанном в Стэнфорде с использованием Джон Алан Робинсон с разрешающая способность принцип. Это была первая автоматизированная система дедукции, продемонстрировавшая способность решать математические задачи, о которых было объявлено в Уведомлениях Американского математического общества до того, как решения были официально опубликованы.[нужна цитата ]

Первый заказ Доказательство теорем - одно из наиболее зрелых направлений автоматизированного доказательства теорем. Логика достаточно выразительна, чтобы можно было определять произвольные проблемы, часто достаточно естественным и интуитивно понятным способом. С другой стороны, он все еще частично разрешим, и был разработан ряд надежных и полных исчислений, позволяющих от корки до корки автоматизированные системы.[нужна цитата ] Более выразительная логика, например Логики высшего порядка, позволяют удобно выражать более широкий круг задач, чем логика первого порядка, но доказательство теорем для этих логик развито не так хорошо.[12][13]

Контрольные точки, конкурсы и источники

Качество реализованных систем улучшилось благодаря существованию большой библиотеки стандартных примеров тестов - Библиотеки задач Тысячи задач для доказательства теорем (TPTP).[14] - а также из Конкурс CADE ATP System (CASC), ежегодное соревнование систем первого порядка для многих важных классов задач первого порядка.

Некоторые важные системы (все они выиграли по крайней мере одно соревнование CASC) перечислены ниже.

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

Популярные техники

Программные системы

Смотрите также: Помощник по доказательству § Сравнение, и Категория: Программные системы доказательства теорем
Сравнение
ИмяТип лицензиивеб-сервисБиблиотекаАвтономныйПоследнее обновление (ГГГГ-мм-дд формат )
ACL23-пункт BSDНетНетдаМай 2019
Prover9 / ВыдраВсеобщее достояниеЧерез Система на TPTPдаНет2009
МетисЛицензия MITНетдаНет1 марта 2018 г.
МетиТарскиМассачусетский технологический институтЧерез Система на TPTPдада21 октября 2014 г.
Jape GPLv2дадаНет15 мая 2015
ПВС GPLv2НетдаНет14 января 2013 г.
Лев IIЛицензия BSDЧерез Система на TPTPдада2013
EQP?НетдаНетМай 2009 г.
ГРУСТНЫЙ GPLv3дадаНет27 августа 2008 г.
PhoX?НетдаНет28 сентября 2017 г.
КеймаераGPLЧерез Веб-запуск Javaдада11 марта 2015 г.
Гэндальф?НетдаНет2009
EGPLЧерез Система на TPTPНетда4 июля 2017 г.
СНАРК Общественная лицензия Mozilla 1.1НетдаНет2012
ВампирЛицензия вампираЧерез Система на TPTPдада14 декабря 2017 г.
Система доказательства теорем (TPS)Соглашение о распространении TPSНетдаНет4 февраля 2012 г.
СПАССЛицензия FreeBSDдададаНоябрь 2005 г.
IsaPlannerGPLНетдада2007
КлючGPLдадада11 октября 2017 г.
Принцессаlgpl v2.1Через Веб-запуск Java и Система на TPTPдада27 января 2018 г.
iProverGPLЧерез Система на TPTPНетда2018
Мета-теоремаБесплатное ПОНетНетдаАпрель 2020
Z3 Доказательство теоремЛицензия MITдадада19 ноября 2019 г.,

Бесплатно программное обеспечение

Проприетарное программное обеспечение

Смотрите также

Примечания

  1. ^ Фреге, Готтлоб (1879). Begriffsschrift. Verlag Louis Neuert.
  2. ^ Фреге, Готтлоб (1884). Die Grundlagen der Arithmetik (PDF). Бреслау: Вильгельм Кобнер. Архивировано из оригинал (PDF) на 2007-09-26. Получено 2012-09-02.
  3. ^ Бертран Рассел; Альфред Норт Уайтхед (1910–1913). Principia Mathematica (1-е изд.). Издательство Кембриджского университета.
  4. ^ Бертран Рассел; Альфред Норт Уайтхед (1927). Principia Mathematica (2-е изд.). Издательство Кембриджского университета.
  5. ^ Эрбранд, Жак (1930). Recherches sur la théorie de la démonstration.
  6. ^ Пресбургер, Mojżesz (1929). "Uber die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem ​​die Addition als einzige Operation hervortritt". Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves. Варшава: 92–101.
  7. ^ а б c d Дэвис, Мартин (2001), «Ранняя история автоматизированного дедукции», в Робинсон, Алан; Воронков Андрей (ред.), Справочник по автоматическому мышлению, 1, Эльзевир)
  8. ^ Бибель, Вольфганг (2007). «Ранняя история и перспективы автоматизированного дедукции» (PDF). Ki 2007. LNAI. Спрингер (4667): 2–18. Получено 2 сентября 2012.
  9. ^ Гилмор, Пол (1960). «Процедура доказательства для теории квантификации: ее обоснование и реализация». Журнал исследований и разработок IBM. 4: 28–35. Дои:10.1147 / пат.41.0028.
  10. ^ W.W. МакКьюн (1997). «Решение проблемы Роббинса». Журнал автоматизированных рассуждений. 19 (3): 263–276. Дои:10.1023 / А: 1005843212881.
  11. ^ Джина Колата (10 декабря 1996 г.). «Доказательство компьютерной математики демонстрирует силу рассуждений». Нью-Йорк Таймс. Получено 2008-10-11.
  12. ^ Кербер, Манфред. "Как доказать теоремы высшего порядка в логике первого порядка." (1999).
  13. ^ Benzmüller, Christoph, et al. "LEO-II - кооперативная программа автоматического доказательства теорем для классической логики высокого порядка (описание системы). »Международная совместная конференция по автоматизированному мышлению. Springer, Берлин, Гейдельберг, 2008.
  14. ^ Сатклифф, Джефф. «Библиотека задач TPTP для автоматизированного доказательства теорем». Получено 15 июля 2019.
  15. ^ Банди, Алан. Автоматизация доказательства математической индукцией. 1999.
  16. ^ Артоси, Альберто, Паола Каттабрига и Гвидо Губернаторори. "Кед: деонтический инструмент для доказательства теорем. »Одиннадцатая Международная конференция по логическому программированию (ICLP’94). 1994.
  17. ^ Оттен, Йенс; Бибель, Вольфганг (2003). «LeanCoP: бережливое доказательство теорем на основе соединений». Журнал символических вычислений. 36 (1–2): 139–161. Дои:10.1016 / S0747-7171 (03) 00037-3.
  18. ^ дель Серро, Луис Фаринас и др. "Lotrec: универсальная программа проверки таблиц для модальных логик и логик описания. »Международная объединенная конференция по автоматизированному мышлению. Springer, Берлин, Гейдельберг, 2001.
  19. ^ Хики, Джейсон и др. "MetaPRL - модульная логическая среда. »Международная конференция по доказательству теорем в логиках высокого порядка. Springer, Berlin, Heidelberg, 2003.
  20. ^ [1] Документация по системе Mathematica

Рекомендации

  • Чин-Лян Чанг; Ричард Чар-Тунг Ли (1973). Символьная логика и механическое доказательство теорем. Академическая пресса.
  • Ловленд, Дональд В. (1978). Автоматическое доказательство теорем: логическая основа. Фундаментальные исследования в области компьютерных наук, том 6. Издательство Северной Голландии.
  • Лакхэм, Дэвид (1990). Программирование со спецификациями: введение в Anna, язык для спецификации программ Ada. Тексты и монографии Springer-Verlag по информатике, 421 стр. ISBN  978-1461396871.

внешняя ссылка