stringtranslate.com

Автоматизированное доказательство теорем

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

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

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

В 1929 году Мойжес Пресбургер показал, что теория натуральных чисел первого порядка со сложением и равенством (теперь называемая арифметикой Пресбургера в его честь) разрешима , и предложил алгоритм, который мог определить, было ли данное предложение на языке истинным или ложным. [6] [7]

Однако вскоре после этого положительного результата Курт Гёдель опубликовал «О формально неразрешимых суждениях принципов математики и родственных систем» (1931), показав, что в любой достаточно сильной аксиоматической системе есть истинные утверждения, которые не могут быть доказаны в этой системе. Эта тема получила дальнейшее развитие в 1930-х годах Алонзо Чёрча и Алана Тьюринга , которые, с одной стороны, дали два независимых, но эквивалентных определения вычислимости , а с другой — привели конкретные примеры неразрешимых вопросов .

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

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

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

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

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

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

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

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

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

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

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

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

Приложения

Автоматизированные средства доказательства теорем были интегрированы с помощниками по доказательству , включая Isabelle/HOL . [12]

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

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

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

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

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

Отношения с СМТ

Существует существенное совпадение между автоматизированными средствами доказательства теорем первого порядка и решателями SMT . Как правило, автоматизированные средства доказательства теорем сосредотачиваются на поддержке полной логики первого порядка с помощью кванторов, тогда как средства решения SMT больше сосредотачиваются на поддержке различных теорий (интерпретируемых символов предикатов). ATP превосходно справляются с задачами с большим количеством кванторов, тогда как решатели SMT хорошо справляются с большими задачами без кванторов. [19] Граница достаточно размыта: некоторые ATP участвуют в SMT-COMP, а некоторые решатели SMT участвуют в CASC . [20]

Бенчмарки, соревнования и источники

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

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

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

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

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

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

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

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

Примечания

  1. ^ Фреге, Готтлоб (1879). Бегриффсшрифт. Верлаг Луи Нойерт.
  2. ^ Фреге, Готтлоб (1884). Die Grundlagen der Arithmetik (PDF) . Бреслау: Вильгельм Кобнер. Архивировано из оригинала (PDF) 26 сентября 2007 г. Проверено 2 сентября 2012 г.
  3. ^ Рассел, Бертран; Уайтхед, Альфред Норт (1910–1913). Principia Mathematica (1-е изд.). Издательство Кембриджского университета.
  4. ^ Рассел, Бертран; Уайтхед, Альфред Норт (1927). Principia Mathematica (2-е изд.). Издательство Кембриджского университета.
  5. ^ Эрбран, Дж. (1930). Recherches sur la theorie de la démonstration (PhD) (на французском языке). Парижский университет.
  6. ^ Пресбургер, Мойжес (1929). «Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, в welchem ​​die Additions als einzige Operation hervortritt». Comptes Rendus du I Congrès de Mathématiciens de Pays рабов . Варшава: 92–101.
  7. ^ abcd Дэвис, Мартин (2001). «Ранняя история автоматизированного дедукции». Робинсон и Воронков 2001 . Архивировано из оригинала 28 июля 2012 г. Проверено 8 сентября 2012 г.
  8. ^ Бибель, Вольфганг (2007). «Ранняя история и перспективы автоматизированного дедукции» (PDF) . Ки 2007 года . ЛНАИ. Спрингер (4667): 2–18. Архивировано (PDF) из оригинала 9 октября 2022 г. Проверено 2 сентября 2012 г.
  9. ^ Гилмор, Пол (1960). «Процедура доказательства количественной теории: ее обоснование и реализация». Журнал исследований и разработок IBM . 4 : 28–35. дои : 10.1147/рд.41.0028.
  10. ^ МакКьюн, WW (1997). «Решение проблемы Роббинса». Журнал автоматизированного рассуждения . 19 (3): 263–276. дои : 10.1023/А: 1005843212881. S2CID  30847540.
  11. ↑ Колата, Джина (10 декабря 1996 г.). «Компьютерное математическое доказательство демонстрирует силу рассуждения». Нью-Йорк Таймс . Проверено 11 октября 2008 г.
  12. ^ Мэн, Цзя; Полсон, Лоуренс К. (1 января 2008 г.). «Перевод предложений высшего порядка в предложения первого порядка». Журнал автоматизированного рассуждения . 40 (1): 35–60. doi : 10.1007/s10817-007-9085-y. ISSN  1573-0670. S2CID  7716709.
  13. ^ Лакхэм, Дэвид С.; Судзуки, Норихиса (март 1976 г.). Автоматическая проверка программы V: Правила доказательства, ориентированные на проверку для массивов, записей и указателей (Технический отчет AD-A027 455). Центр оборонной технической информации . Архивировано из оригинала 12 августа 2021 года.
  14. ^ Лакхэм, Дэвид С.; Судзуки, Норихиса (октябрь 1979 г.). «Проверка операций с массивами, записями и указателями в Паскале». Транзакции ACM в языках и системах программирования . 1 (2): 226–244. дои : 10.1145/357073.357078 . S2CID  10088183.
  15. ^ Лакхэм, Д.; Герман, С.; фон Хенке, Ф.; Карп, Р.; Милн, П.; Оппен, Д.; Полак, В.; Шерлис, В. (1979). Руководство пользователя верификатора Stanford Pascal (Технический отчет). Стэндфордский Университет. CS-TR-79-731.
  16. ^ Лавленд, DW (1986). «Автоматическое доказательство теорем: отображение логики в ИИ». Материалы международного симпозиума ACM SIGART по методологиям интеллектуальных систем . Ноксвилл, Теннесси, США: ACM Press. п. 224. дои : 10.1145/12808.12833 . ISBN 978-0-89791-206-8. S2CID  14361631.
  17. ^ Кербер, Манфред. «Как доказать теоремы высшего порядка в логике первого порядка». (1999).
  18. ^ Бенцмюллер, Кристоф и др. «LEO-II — кооперативное автоматическое средство доказательства теорем для классической логики высшего порядка (описание системы)». Международная совместная конференция по автоматизированному рассуждению. Берлин, Германия и Гейдельберг: Springer, 2008.
  19. ^ Бланшетт, Жасмин Кристиан; Бёме, Саша; Полсон, Лоуренс К. (01 июня 2013 г.). «Расширение Sledgehammer с помощью SMT Solvers». Журнал автоматизированного рассуждения . 51 (1): 109–128. дои : 10.1007/s10817-013-9278-5. ISSN  1573-0670. S2CID  5389933. Решатели ATP и SMT имеют взаимодополняющие преимущества. Первые более элегантно справляются с квантификаторами, тогда как вторые превосходно справляются с большими, в основном наземными задачами.
  20. ^ Вебер, Тьярк; Коншон, Сильвен; Дехарб, Давид; Хейцманн, Матиас; Нимец, Айна; Регер, Джайлз (01 января 2019 г.). «Конкурс СМТ 2015–2018». Журнал по выполнимости, логическому моделированию и вычислениям . 11 (1): 221–259. дои : 10.3233/SAT190123 . В последние годы мы наблюдаем стирание границ между SMT-COMP и CASC: решатели SMT конкурируют в CASC, а ATP — в SMT-COMP.
  21. ^ Сатклифф, Джефф. «Библиотека задач TPTP для автоматического доказательства теорем» . Проверено 15 июля 2019 г.
  22. ^ «История». vprover.github.io .
  23. ^ "Музей Доказательства теорем" . Майкл Кольхазе . Проверено 20 ноября 2022 г.
  24. ^ Банди, Алан (1999). Автоматизация доказательства методом математической индукции (PDF) (Технический отчет). Отчет об исследовании информатики. Том. 2. Отделение информатики Эдинбургского университета. hdl : 1842/3394.
  25. ^ Габбай, Дов М. и Ханс Юрген Ольбах. «Устранение кванторов в логике предикатов второго порядка». (1992).

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

Внешние ссылки