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

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

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

В то время как корни формализованной логики восходят к Аристотелю , в конце 19-го и начале 20-го веков появилась современная логика и формализованная математика. Фреге «s Begriffsschrift (1879) представил как полное исчисление высказываний и то , что, по существу , современная логика предикатов . Его « Основы арифметики» , опубликованные в 1884 году, выражают (части) математики в формальной логике. Этот подход был продолжен Расселом и Уайтхедом в их влиятельных « Принципах математики» , впервые опубликованных в 1910–1913 гг., А также в пересмотренном втором издании в 1927 г. Рассел и Уайтхед считали, что они могут вывести всю математическую истину, используя аксиомы и правила вывода формальной логики, в принципе открытие процесса автоматизации. В 1920 годе Туральф Скуль упрощен предыдущий результат на Leopold Левенгейм , что приводит к теореме Левенгейм-сколемовской , а в 1930 г. к понятию Вселенной Эрбрана и интерпретации Эрбрана , что позволило (ООН) выполнимости формул первого порядка (и , следовательно , справедливость теоремы) сводиться к (потенциально бесконечно много) пропозициональных проблемы выполнимости.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Примечания

использованная литература

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

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