Войти
Автоматическое доказательство теорем (также известное как ATP или автоматическое вычисление ) является подполем автоматических рассуждений и математической логики, имеющим дело с доказательством математических теорем с помощью компьютерных программ. Автоматические рассуждения над математическим доказательством послужили основным стимулом для развития информатики.
Хотя корни формализованной логики уходят в прошлое до Аристотеля, конец 19 - начало 20 веков ознаменовались развитием современной логики и формализованной математики. Фреге Begriffsschrift (1879) представил как полное исчисление высказываний, так и то, что по сути является современной логикой предикатов. Его Основы арифметики, опубликованные в 1884 году, выразили (части) математики в формальной логике. Этот подход был продолжен Расселом и Уайтхедом в их влиятельных Principia Mathematica, впервые опубликованных в 1910–1913 гг., А во втором пересмотренном издании - в 1927 г. Рассел и Уайтхед. думали, что они могут вывести всю математическую истину, используя аксиомы и правила вывода формальной логики, в принципе открывая процесс для автоматизации. В 1920 году Торальф Сколем упростил предыдущий результат Леопольдом Левенхаймом, что привело к теореме Лёвенгейма – Сколема, а в 1930 году к понятию Вселенная Эрбрана и интерпретация Эрбрана, которая позволила (не) выполнимость формул первого порядка (и, следовательно, справедливость теоремы) быть сведена к (потенциально бесконечно много) проблемы пропозициональной выполнимости.
В 1929 году Моджес Пресбургер показал, что теория натуральных чисел со сложением и равенством (теперь называется арифметикой Пресбургера в его честь) разрешима и дал алгоритм, который мог определить, было ли данное предложение на языке истинным или ложным. Однако вскоре после этого положительного результата Курт Гёдель опубликовал О формально неразрешимых предложениях Principia Mathematica и связанных систем (1931), показывая, что в любой достаточно сильной аксиоматической системе есть истинные утверждения, которые не может быть доказано в системе. Эта тема получила дальнейшее развитие в 1930-х годах Алонзо Черч и Аланом Тьюрингом, которые, с одной стороны, дали два независимых, но эквивалентных определения вычислимости, а также другие дали конкретные примеры для неразрешимых вопросов.
Вскоре после Второй мировой войны появились первые компьютеры общего назначения. В 1954 году Мартин Дэвис запрограммировал алгоритм Пресбургера для компьютера с электронными лампами JOHNNIAC в Принстонском институте перспективных исследований. По словам Дэвиса, «его большим триумфом было доказательство того, что сумма двух четных чисел является четной». Более амбициозной была Logic Theory Machine в 1956 году, система дедукции для логики высказываний Principia Mathematica, разработанная Алленом Ньюэллом, Гербертом А.. Саймон и Дж. К. Шоу. Также работающая на JOHNNIAC, машина логической теории построила доказательства из небольшого набора пропозициональных аксиом и трех правил дедукции: modus ponens, (пропозициональная) подстановка переменных и замена формул по их определению. Система использовала эвристическое руководство и смогла доказать 38 из первых 52 теорем Принципов.
«Эвристический» подход Логической Теоретической Машины пытался подражать человеческим математикам и не мог гарантировать, что доказательство сможет можно найти для каждой справедливой теоремы, даже в принципе. Напротив, другие, более систематические алгоритмы достигают, по крайней мере теоретически, полноты для логики первого порядка. Первоначальные подходы основывались на результатах Хербранда и Сколема для преобразования формулы первого порядка в последовательно увеличивающиеся наборы пропозициональных формул путем создания экземпляров переменных с терминами из вселенной Хербранда. Затем пропозициональные формулы могут быть проверены на неудовлетворительность с помощью ряда методов. Программа Гилмора использовала преобразование в дизъюнктивную нормальную форму, форму, в которой выполнимость формулы очевидна.
В зависимости от лежащей в основе логики Проблема определения действительности формулы варьируется от тривиальной до невозможной. Для частого случая логики высказываний проблема разрешима, но NP-полная, и, следовательно, предполагается, что для общих задач доказательства существуют только алгоритмы экспоненциального времени. Для исчисления предикатов первого порядка, теорема Гёделя утверждает, что теоремы (доказуемые утверждения) являются в точности логически действительными правильно сформированными формулами, таким образом идентифицируя действительные формулы является рекурсивно перечислимым : с учетом неограниченных ресурсов любая действительная формула может быть в конечном итоге доказана. Однако неверные формулы (те, которые не вытекают из данной теории) не всегда могут быть распознаны.
Вышеизложенное применимо к теориям первого порядка, таким как арифметика Пеано. Однако для конкретной модели, которая может быть описана теорией первого порядка, некоторые утверждения могут быть верными, но неразрешимыми в теории, используемой для описания модели. Например, по теореме Гёделя о неполноте мы знаем, что любая теория, собственные аксиомы которой верны для натуральных чисел, не может доказать, что все утверждения первого порядка верны для натуральных чисел, даже если список собственных аксиом может быть бесконечным перечислимым. Отсюда следует, что автоматическое средство доказательства теорем не сможет завершить поиск доказательства именно тогда, когда исследуемое утверждение неразрешимо в используемой теории, даже если оно истинно в интересующей модели. Несмотря на этот теоретический предел, на практике средства доказательства теорем могут решать множество сложных задач, даже в моделях, которые не полностью описываются какой-либо теорией первого порядка (например, целые числа).
Более простая, но связанная проблема - это проверка доказательства, когда существующее доказательство теоремы удостоверяется действительным. Для этого обычно требуется, чтобы каждый отдельный шаг проверки мог быть проверен с помощью примитивной рекурсивной функции или программы, и, следовательно, проблема всегда разрешима.
Поскольку доказательства, генерируемые автоматическими средствами доказательства теорем, обычно очень велики, проблема сжатия доказательств имеет решающее значение, и различные методы, направленные на то, чтобы сделать результат доказывающего меньше, и, следовательно, более легким для понимания и проверки., были разработаны.
Помощники проверки требуют, чтобы пользователь-человек давал системе подсказки. В зависимости от степени автоматизации, доказывающая сторона может быть по существу сведена к проверке доказательства, при этом пользователь предоставляет доказательство формальным образом, или важные задачи доказательства могут выполняться автоматически. Интерактивные средства доказательства используются для множества задач, но даже полностью автоматические системы доказали ряд интересных и трудных теорем, включая по крайней мере одну, которая долгое время ускользала от математиков, а именно гипотезу Роббинса. Однако эти успехи случаются нерегулярно, и для решения сложных проблем обычно требуется опытный пользователь.
Другое различие иногда проводится между доказательством теорем и другими методами, когда процесс считается доказательством теоремы, если он состоит из традиционного доказательства, начиная с аксиом и производя новые шаги вывода с использованием правил вывода. Другие методы могут включать проверку модели, которая, в простейшем случае, включает в себя перебор многих возможных состояний (хотя фактическая реализация средств проверки модели требует большого ума и не сводится просто к грубой силе).
Существуют гибридные системы доказательства теорем, которые используют проверку модели в качестве правила вывода. Существуют также программы, которые были написаны для доказательства конкретной теоремы с (обычно неформальным) доказательством того, что если программа завершается с определенным результатом, то теорема верна. Хорошим примером этого было машинное доказательство теоремы о четырех цветах, которое было очень спорным как первое заявленное математическое доказательство, которое было практически невозможно проверить людьми из-за огромного размера вычислений программы. (такие доказательства называются неотслеживаемыми доказательствами ). Другой пример программного доказательства - это тот, который показывает, что игру Connect Four всегда может выиграть первый игрок.
Коммерческое использование автоматического доказательства теорем в основном сосредоточено в разработке интегральных схем и проверке. Начиная с ошибки Pentium FDIV, сложные блоки с плавающей запятой современных микропроцессоров были разработаны с особой тщательностью. AMD, Intel и другие используют автоматическое доказательство теорем, чтобы убедиться, что деление и другие операции правильно реализованы в их процессорах.
В конце 1960-х годов агентства, финансирующие исследования в области автоматизированной дедукции, начали подчеркивать необходимость практического применения. Одной из первых плодотворных областей была проверка программ, при которой средства доказательства теорем первого порядка применялись к проблеме проверки правильности компьютерных программ на таких языках, как Паскаль, Ада и т. Д. Известная среди ранних программ проверки. систем был Stanford Pascal Verifier, разработанный Дэвидом Лакхэмом в Стэнфордском университете. Это было основано на Стэнфордском устройстве доказательства разрешающей способности, также разработанном в Стэнфорде с использованием принципа разрешения Джона Алана Робинсона. Это была первая автоматизированная система вывода, продемонстрировавшая способность решать математические задачи, о которых было объявлено в Уведомлениях Американского математического общества до того, как решения были официально опубликованы.
Доказательство теорем первого порядка является одним из наиболее зрелых подполей. автоматизированного доказательства теорем. Логика достаточно выразительна, чтобы можно было описывать произвольные проблемы, часто достаточно естественным и интуитивно понятным способом. С другой стороны, это все еще полуразрешимо, и был разработан ряд надежных и полных исчислений, позволяющих использовать полностью автоматизированные системы. Более выразительные логики, такие как логики высшего порядка, позволяют удобно выражать более широкий круг проблем, чем логика первого порядка, но доказательство теорем для этих логик развито не так хорошо.
Качество реализованных систем повысилось благодаря существованию большой библиотеки стандартных примеров тестов - Библиотеки задач Тысячи задач для программы доказательства теорем (TPTP), а также библиотеки CADE ATP System Competition (CASC), ежегодное соревнование систем первого порядка для многих важных классов задач первого порядка.
Некоторые важные системы (все они выиграли хотя бы одно соревнование CASC) перечислены ниже.
Музей средства доказательства теорем - это инициатива по сохранению источников систем доказательства теорем для будущего анализа, поскольку они являются важными культурными / научными артефактами. Он имеет источники многих из упомянутых выше систем.
| Имя | Тип лицензии | Веб-сервис | Библиотека | Автономная | Последнее обновление (формат YYYY-mm-dd ) |
|---|---|---|---|---|---|
| ACL2 | 3-clause BSD | No | No | Да | май 2019 г. |
| Prover9 / Otter | Public Domain | Через систему на TPTP | Да | No | 2009 |
| Лицензия Metis | MIT | No | Да | No | 1 марта 2018 г. |
| MetiTarski | MIT | Через систему на TPTP | Да | Да | Октябрь 21, 2014 |
| Jape | GPLv2 | Да | Да | No | 15 мая 2015 года |
| PVS | GPLv2 | No | Да | No | 14 января 2013 |
| Leo II | Лицензия BSD | Через систему на TPTP | Да | Да | 2013 |
| EQP | ? | No | Да | No | Май 2009 г. |
| SAD | GPLv3 | Да | Да | No | 27 августа 2008 г. |
| PhoX | ? | No | Да | No | 28 сентября 2017 г. |
| Кеймаера | GPL | Через Java Webstart | Да | Да | 11 марта 2015 г. |
| ? | No | Да | No | 2009 | |
| E | GPL | Через систему на TPTP | No | Да | 4 июля, 2017 |
| SNARK | Общественная лицензия Mozilla 1.1 | No | Да | No | 2012 |
| Vampire | Лицензия Vampire | Через систему на TPTP | Да | Да | 14 декабря 2017 г. |
| Система доказательства теорем (TPS) | Соглашение о распространении TPS | No | Да | No | 4 февраля 2012 г. |
| SPASS | Лицензия FreeBSD | Да | Да | Да | Ноябрь 2005 г. |
| IsaPlanner | GPL | No | Да | Да | 2007 |
| KeY | GPL | Да | Да | Да | 11 октября 2017 года |
| Princess | lgpl v2.1 | Через Java Webstart и Система на TPTP | Да | Да | 27 января 2018 г. |
| iProver | GPL | Через Система на TPTP | No | Да | 2018 |
| Мета теорема | Бесплатное ПО | No | No | Да | Апрель 2020 |
| Z3 Теорема Доказательство | Лицензия MIT | Да | Да | Да | 19 ноября 2019 г. |
