Автоматизированное доказательство теорем
Автоматическое доказательство теорем (также известное как ATP или автоматизированный вывод ) — это подобласть автоматизированных рассуждений и математической логики, занимающаяся доказательством математических теорем с помощью компьютерных программ . Автоматизированное рассуждение по поводу математического доказательства стало основным стимулом для развития информатики .
Логические основы [ править ]
Хотя корни формализованной логики восходят к Аристотелю , в конце 19 и начале 20 веков наблюдалось развитие современной логики и формализованной математики. В книге Фреге « 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 всегда может выиграть первый игрок.
Приложения [ править ]
Коммерческое использование автоматизированного доказательства теорем в основном сосредоточено на интегральных схем проектировании и проверке . После появления ошибки Pentium FDIV сложные блоки с плавающей запятой в современных микропроцессорах разрабатывались с особой тщательностью. AMD , Intel и другие компании используют автоматизированное доказательство теорем, чтобы убедиться, что деление и другие операции правильно реализованы в их процессорах. [12]
Другое использование средств доказательства теорем включает синтез программ , построение программ, удовлетворяющих формальным спецификациям . [13] Автоматизированные средства доказательства теорем были интегрированы с помощниками по доказательству , включая Isabelle/HOL . [14]
Приложения средств доказательства теорем также можно найти в обработке естественного языка и формальной семантике , где они используются для анализа представлений дискурса . [15] [16]
Доказательство теорем первого порядка [ править ]
В конце 1960-х годов агентства, финансирующие исследования в области автоматизированного вывода, начали подчеркивать необходимость практического применения. [ нужна ссылка ] Одной из первых плодотворных областей была область верификации программ , где средства доказательства теорем первого порядка применялись к проблеме проверки правильности компьютерных программ на таких языках, как Паскаль , Ада и т. д. Среди ранних систем верификации программ примечательной была система Stanford Pascal Verifier. разработан Дэвидом Лакхемом из Стэнфордского университета . [17] [18] [19] Это было основано на Стэнфордском средстве проверки разрешения, также разработанном в Стэнфорде с использованием Джона Алана Робинсона принципа разрешения . Это была первая автоматизированная система дедукции, продемонстрировавшая способность решать математические задачи, о которых было объявлено в Уведомлениях Американского математического общества до того, как решения были официально опубликованы. [ нужна ссылка ]
Доказательство теорем первого порядка — одна из наиболее зрелых областей автоматизированного доказательства теорем. Логика достаточно выразительна, чтобы позволить определять произвольные задачи, часто достаточно естественным и интуитивным способом. С другой стороны, она все еще полуразрешима, и был разработан ряд надежных и полных расчетов, позволяющих полностью автоматизировать системы. [20] Более выразительные логики, такие как логики высшего порядка , позволяют удобно выражать более широкий круг задач, чем логика первого порядка, но доказательство теорем для этих логик менее развито. [21] [22]
с SMT Отношения
Существует существенное совпадение между автоматизированными средствами доказательства теорем первого порядка и решателями SMT . Как правило, автоматизированные средства доказательства теорем сосредотачиваются на поддержке полной логики первого порядка с помощью кванторов, тогда как средства решения SMT больше сосредотачиваются на поддержке различных теорий (интерпретируемых символов предикатов). ATP превосходно справляются с задачами с большим количеством кванторов, тогда как решатели SMT хорошо справляются с большими задачами без кванторов. [23] Граница настолько размыта, что некоторые ATP участвуют в SMT-COMP, а некоторые решатели SMT участвуют в CASC . [24]
Тесты, соревнования и источники [ править ]
Качество реализованных систем улучшилось благодаря существованию большой библиотеки стандартных эталонных примеров — «Тысячи задач для доказывающих теорем» (TPTP). библиотеки задач [25] - а также на конкурсе систем CADE ATP (CASC), ежегодном конкурсе систем первого порядка для многих важных классов задач первого порядка.
Некоторые важные системы (все они выиграли хотя бы один дивизион соревнований CASC) перечислены ниже.
- E — это высокопроизводительное средство доказательства для полной логики первого порядка, но построенное на чисто эквациональном исчислении , первоначально разработанное в группе автоматизированных рассуждений Мюнхенского технического университета под руководством Вольфганга Бибеля , а теперь в Кооперативном государственном университете Баден-Вюртемберга. в Штутгарте .
- Otter , разработанный в Аргоннской национальной лаборатории , основан на разрешении первого порядка и парамодуляции . С тех пор Otter был заменен на Prover9 , который работает в паре с Mace4 .
- SETHEO — это высокопроизводительная система, основанная на целенаправленном исчислении исключения моделей , первоначально разработанная командой под руководством Вольфганга Бибеля . E и SETHEO были объединены (с другими системами) в составное средство доказательства теорем E-SETHEO.
- Первоначально Vampire был разработан и реализован в Манчестерском университете Андреем Воронковым и Криштофом Ходером. Сейчас он разрабатывается растущей международной командой. С 2001 года он регулярно выигрывал дивизион FOF (среди других дивизионов) на соревнованиях по системе CADE ATP. [26]
- Waldmeister — это специализированная система логики первого порядка с единичными уравнениями, разработанная Арнимом Бухом и Томасом Хилленбрандом. Он выигрывал дивизион CASC UEQ четырнадцать лет подряд (1997–2010).
- SPASS — это средство доказательства логических теорем первого порядка с равенством. Он разработан исследовательской группой «Автоматизация логики» Института компьютерных наук Макса Планка .
Музей доказательства теорем [27] — это инициатива по сохранению источников систем доказательства теорем для будущего анализа, поскольку они являются важными культурными/научными артефактами. Он содержит исходные коды многих систем, упомянутых выше.
Популярные техники [ править ]
 |
- Разрешение первого порядка с унификацией
- Удаление модели
- Метод аналитических таблиц
- Суперпозиция и переписывание терминов
- Проверка модели
- Математическая индукция [28]
- Бинарные диаграммы решений
- ДПЛЛ
- Объединение высшего порядка
- Удаление квантификатора [29]
Программные системы [ править ]
Бесплатное программное обеспечение [ править ]
- Альт-Эрго
- Автомат
- КВК
- И
- IsaPlanner
- LCF
- Плотник
- НуПРЛ
- Парадокс
- Prover9
- ПВС
- СПАРК (язык программирования)
- Двенадцать
- Теорема Z3
Собственное программное обеспечение [ править ]
См. также [ править ]
- Переписка Карри-Ховарда
- Символьное вычисление
- Машина Рамануджана
- Компьютерное доказательство
- Формальная проверка
- Логическое программирование
- Проверка доказательств
- Проверка модели
- Сложность доказательства
- Система компьютерной алгебры
- Программный анализ (информатика)
- Общее решение проблем
- Метаматический язык для формализованной математики
- Фактор Брюйна
Примечания [ править ]
- ^ Фреге, «Хвала Богу» (1879). Концептуальное письмо . Издатель Луи Нойерт.
- ^ Фреге, Готтлоб (1884). Основы арифметики (PDF) . Бреслау: Вильгельм Кобнер. Архивировано из оригинала (PDF) 26 сентября 2007 г. Проверено 2 сентября 2012 г.
- ^ Рассел, Бертран; Уайтхед, Альфред Норт (1910–1913). Principia Mathematica (1-е изд.). Издательство Кембриджского университета.
- ^ Рассел, Бертран; Уайтхед, Альфред Норт (1927). Principia Mathematica (2-е изд.). Издательство Кембриджского университета.
- ^ Эрбран, Ж. (1930). Исследования по теории демонстрации (PhD) (на французском языке). Парижский университет.
- ^ Пресбургер, Мойжес (1929). «О полноте некоторой системы арифметики целых чисел, в которой единственным действием является сложение». Comptes Rendus du I Congrès de Mathematiciens des Pays рабов . Варшава: 92-101.
- ↑ Перейти обратно: Перейти обратно: а б с д Дэвис, Мартин (2001). «Ранняя история автоматизированного дедукции» . Робинсон и Воронков 2001 . Архивировано из оригинала 28 июля 2012 г. Проверено 8 сентября 2012 г.
- ^ Бибель, Вольфганг (2007). «Ранняя история и перспективы автоматизированного дедукции» (PDF) . Ки 2007 года . ЛНАИ (4667). Спрингер: 2–18. Архивировано (PDF) из оригинала 9 октября 2022 г. Проверено 2 сентября 2012 г.
- ^ Гилмор, Пол (1960). «Процедура доказательства количественной теории: ее обоснование и реализация». Журнал исследований и разработок IBM . 4 : 28–35. дои : 10.1147/рд.41.0028 .
- ^ МакКьюн, WW (1997). «Решение проблемы Роббинса». Журнал автоматизированного рассуждения . 19 (3): 263–276. дои : 10.1023/А:1005843212881 . S2CID 30847540 .
- ^ Колата, Джина (10 декабря 1996 г.). «Компьютерное математическое доказательство демонстрирует силу рассуждения» . Нью-Йорк Таймс . Проверено 11 октября 2008 г.
- ^ Гоэл, Шилпи; Рэй, Сандип (2022), Чаттопадхьяй, Анупам (редактор), «Гарантия микропроцессора и роль доказательства теорем» , Справочник по компьютерной архитектуре , Сингапур: Springer Nature Singapore, стр. 1–43, doi : 10.1007/978-981 -15-6401-7_38-1 , ISBN 978-981-15-6401-7 , получено 10 февраля 2024 г.
- ^ Басин, Д.; Девиль, Ю.; Фленер, П.; Хамфельт, А.; Фишер Нильссон, Дж. (2004). «Синтез программ вычислительной логики». У М. Брюйноге и К.-К. Лау (ред.). Разработка программ по вычислительной логике . ЛНКС. Том. 3049. Спрингер. стр. 30–65. CiteSeerX 10.1.1.62.4976 .
- ^ Мэн, Цзя; Полсон, Лоуренс К. (1 января 2008 г.). «Перевод предложений высшего порядка в предложения первого порядка» . Журнал автоматизированного рассуждения . 40 (1): 35–60. дои : 10.1007/s10817-007-9085-y . ISSN 1573-0670 . S2CID 7716709 .
- ^ Бос, Йохан. «Широкий семантический анализ с участием боксера». Семантика в обработке текста. Шаг 2008 Материалы конференции. 2008.
- ^ Маскенс, Рейнхард. «Объединение семантики Монтегю и репрезентации дискурса». Лингвистика и философия (1996): 143-186.
- ^ Лакхэм, Дэвид К.; Судзуки, Норихиса (март 1976 г.). Автоматическая проверка программы V: Правила доказательства, ориентированные на проверку для массивов, записей и указателей (Технический отчет AD-A027 455). Центр оборонной технической информации . Архивировано из оригинала 12 августа 2021 года.
- ^ Лакхэм, Дэвид К.; Судзуки, Норихиса (октябрь 1979 г.). «Проверка операций с массивами, записями и указателями в Паскале» . Транзакции ACM в языках и системах программирования . 1 (2): 226–244. дои : 10.1145/357073.357078 . S2CID 10088183 .
- ^ Лакхэм, Д.; Герман, С.; фон Хенке, Ф.; Карп, Р.; Милн, П.; Оппен, Д.; Полак, В.; Шерлис, В. (1979). Руководство пользователя верификатора Stanford Pascal (Технический отчет). Стэнфордский университет. CS-TR-79-731.
- ^ Лавленд, Д.В. (1986). «Автоматическое доказательство теорем: отображение логики в ИИ». Материалы международного симпозиума ACM SIGART по методологиям интеллектуальных систем . Ноксвилл, Теннесси, США: ACM Press. п. 224. дои : 10.1145/12808.12833 . ISBN 978-0-89791-206-8 . S2CID 14361631 .
- ^ Кербер, Манфред. « Как доказать теоремы высшего порядка в логике первого порядка ». (1999).
- ^ Бенцмюллер, Кристоф и др. « LEO-II — кооперативное автоматическое средство доказательства теорем для классической логики высшего порядка (описание системы) ». Международная совместная конференция по автоматизированному рассуждению. Берлин, Германия и Гейдельберг: Springer, 2008.
- ^ Бланшетт, Жасмин Кристиан; Бёме, Саша; Полсон, Лоуренс К. (01 июня 2013 г.). «Расширение Sledgehammer с помощью SMT Solvers» . Журнал автоматизированного рассуждения . 51 (1): 109–128. дои : 10.1007/s10817-013-9278-5 . ISSN 1573-0670 . S2CID 5389933 .
Решатели ATP и SMT имеют взаимодополняющие преимущества. Первые более элегантно справляются с квантификаторами, тогда как вторые превосходно справляются с большими, в основном наземными задачами.
- ^ Вебер, Тьярк; Коншон, Сильвен; Дехарб, Давид; Хейцманн, Матиас; Нимец, Айна; Регер, Джайлз (01 января 2019 г.). «Конкурс СМТ 2015–2018» . Журнал по выполнимости, логическому моделированию и вычислениям . 11 (1): 221–259. дои : 10.3233/SAT190123 .
В последние годы мы наблюдаем стирание границ между SMT-COMP и CASC: решатели SMT конкурируют в CASC, а ATP — в SMT-COMP.
- ^ Сатклифф, Джефф. «Библиотека задач TPTP для автоматического доказательства теорем» . Проверено 15 июля 2019 г.
- ^ «История» . vprover.github.io .
- ^ «Музей доказательства теорем» . Майкл Кольхазе . Проверено 20 ноября 2022 г.
- ^ Банди, Алан (1999). Автоматизация доказательства методом математической индукции (PDF) (Технический отчет). Отчет об исследовании информатики. Том. 2. Отделение информатики Эдинбургского университета. hdl : 1842/3394 .
- ^ Габбай, Дов М. и Ханс Юрген Ольбах. «Устранение кванторов в логике предикатов второго порядка». (1992).
Ссылки [ править ]
- Чанг, Цзинь-Лян; Ли, Ричард Чар-Тунг (2014) [1973]. Символическая логика и механическое доказательство теорем . Эльзевир. ISBN 9780080917283 .
- Лавленд, Дональд В. (2016) [1978]. Автоматизированное доказательство теорем: логическая основа . Фундаментальные исследования в области компьютерных наук. Том. 6. Эльзевир. ISBN 9781483296777 .
- Лакхэм, Дэвид (1990). Программирование со спецификациями: введение в Anna, язык для описания программ Ada . Спрингер. ISBN 978-1461396871 .
- Галье, Жан Х. (2015) [1986]. Логика для информатики: основы автоматического доказательства теорем (2-е изд.). Дувр. ISBN 978-0-486-78082-5 .
Этот материал может быть воспроизведен в любых образовательных целях,...
- Даффи, Дэвид А. (1991). Принципы автоматического доказательства теорем . Уайли. ISBN 9780471927846 .
- Вос, Ларри ; Овербик, Росс; Ласк, Юинг; Бойл, Джим (1992). Автоматизированное рассуждение: введение и применение (2-е изд.). МакГроу-Хилл . ISBN 9780079112514 .
- Робинсон, Алан ; Воронков, Андрей , ред. (2001). Справочник по автоматизированному рассуждению . Том. И. Эльзевир , MIT Press . ISBN 9780080532790 . II ISBN 9780262182232 .
- Фиттинг, Мелвин (2012) [1996]. Логика первого порядка и автоматическое доказательство теорем (2-е изд.). Спрингер. ISBN 9781461223603 .
Внешние ссылки [ править ]
| Базы данных органов управления : Национальные |
|---|
