Автоматическое доказательство теорем (также известное как ATP или автоматическая дедукция ) - это подраздел автоматизированных рассуждений и математической логики, занимающийся доказательством математических теорем с помощью компьютерных программ . Автоматизированное рассуждение над математическим доказательством стало основным стимулом для развития информатики .
Логические основы
В то время как корни формализованной логики восходят к Аристотелю , в конце 19-го и начале 20-го веков появилась современная логика и формализованная математика. Фреге «s Begriffsschrift (1879) представил как полное исчисление высказываний и то , что, по существу , современная логика предикатов . [1] Его « Основы арифметики» , опубликованные в 1884 году, [2] выражают (части) математики в формальной логике. Этот подход был продолжен Расселом и Уайтхедом в их влиятельных « Принципах математики» , впервые опубликованных в 1910–1913 годах [3], а также в пересмотренном втором издании в 1927 году. [4] Рассел и Уайтхед считали, что они могут вывести всю математическую истину, используя аксиомы и правила вывода. формальной логики, в принципе открывая процесс автоматизации. В 1920 годе Туральф Скуль упрощен предыдущий результат на Leopold Левенгейм , что приводит к теореме Левенгейм-сколемовской , а в 1930 г. к понятию Вселенной Эрбрана и интерпретации Эрбрана , что позволило (ООН) выполнимости формул первого порядка (и , следовательно , справедливость теоремы) сводиться к (потенциально бесконечно много) пропозициональных проблемы выполнимости. [5]
В 1929 году Моджеш Пресбургер показал, что теория натуральных чисел со сложением и равенством (теперь называемая арифметикой Пресбургера в его честь) разрешима, и дал алгоритм, который мог определить, было ли данное предложение языка истинным или ложным. [6] [7] Однако вскоре после этого положительного результата Курт Гёдель опубликовал « О формально неразрешимых предложениях принципов математики и родственных систем» (1931 г.), показывая, что в любой достаточно сильной аксиоматической системе есть истинные утверждения, которые невозможно доказать в системе. . Эта тема получила дальнейшее развитие в 1930-х годах Алонзо Черчем и Аланом Тьюрингом , которые, с одной стороны, дали два независимых, но эквивалентных определения вычислимости , а с другой - привели конкретные примеры неразрешимых вопросов.
Первые реализации
Вскоре после Второй мировой войны появились первые компьютеры общего назначения. В 1954 году Мартин Дэвис запрограммировал алгоритм Пресбургера для компьютера на электронных лампах JOHNNIAC в Принстонском институте перспективных исследований . По словам Дэвиса, «его большим триумфом было доказательство того, что сумма двух четных чисел является четной». [7] [8] Более амбициозная была логика Теория машин в 1956 году, система вычетов для логики высказываний в Principia Mathematica , разработанный Аллен Ньюэлл , Герберт А. Саймон и JC Шоу . Также работающая на JOHNNIAC, машина логической теории построила доказательства на основе небольшого набора пропозициональных аксиом и трех правил дедукции: modus ponens , (пропозициональная) подстановка переменных и замена формул по их определению. Система использовала эвристическое руководство и сумела доказать 38 из первых 52 теорем Принципов . [7]
«Эвристический» подход Логической Теоретической Машины пытался подражать человеческим математикам и не мог гарантировать, что доказательство может быть найдено для каждой действительной теоремы даже в принципе. Напротив, другие, более систематические алгоритмы достигли, по крайней мере теоретически, полноты для логики первого порядка. Первоначальные подходы основывались на результатах Хербранда и Сколема для преобразования формулы первого порядка в последовательно увеличивающиеся наборы пропозициональных формул путем создания экземпляров переменных с терминами из вселенной Хербранда . Затем пропозициональные формулы можно было бы проверить на неудовлетворительность с помощью ряда методов. Программа Гилмора использовала преобразование в дизъюнктивную нормальную форму , форму, в которой выполнимость формулы очевидна. [7] [9]
Разрешимость проблемы
В зависимости от лежащей в основе логики проблема определения действительности формулы варьируется от тривиальной до невозможной. Для частого случая логики высказываний проблема разрешима, но совместно NP-полна , и, следовательно, считается, что для общих задач доказательства существуют только алгоритмы экспоненциального времени. Для исчисления предикатов первого порядка , полнота теоремы Гёделя утверждает , что теоремы (доказуемые заявления) в точности логически действующие правильно построенные формулы , так что определение действительных формул перечислимый : учитывая неограниченные ресурсы, любая действительная формула в конечном счете может быть доказана. Однако неверные формулы (те, которые не вытекают из данной теории) не всегда могут быть распознаны.
Сказанное выше относится к теориям первого порядка, таким как арифметика Пеано . Однако для конкретной модели, которая может быть описана теорией первого порядка, некоторые утверждения могут быть верными, но неразрешимыми в теории, используемой для описания модели. Например, по теореме Гёделя о неполноте мы знаем, что любая теория, собственные аксиомы которой верны для натуральных чисел, не может доказать, что все утверждения первого порядка верны для натуральных чисел, даже если список собственных аксиом может быть бесконечным перечислимым. Отсюда следует, что автоматическое средство доказательства теорем не сможет завершить поиск доказательства именно тогда, когда исследуемое утверждение неразрешимо в используемой теории, даже если оно истинно в интересующей модели. Несмотря на этот теоретический предел, на практике средства доказательства теорем могут решать множество сложных задач, даже в моделях, которые не полностью описываются какой-либо теорией первого порядка (например, целые числа).
Связанные проблемы
Более простая, но связанная с этим проблема - это проверка доказательства , когда существующее доказательство теоремы удостоверяется действительным. Для этого обычно требуется, чтобы каждый отдельный шаг доказательства мог быть проверен примитивной рекурсивной функцией или программой, и, следовательно, проблема всегда разрешима.
Поскольку доказательства, генерируемые автоматическими средствами доказательства теорем, обычно очень велики, проблема сжатия доказательств имеет решающее значение, и были разработаны различные методы, направленные на уменьшение вывода средства доказательства и, следовательно, более легкое для понимания и проверки.
Помощники по проверке требуют, чтобы пользователь-человек давал подсказки системе. В зависимости от степени автоматизации, доказывающая сторона может быть сведена к проверке доказательства, когда пользователь предоставляет доказательство формальным образом, или важные задачи доказательства могут выполняться автоматически. Интерактивные средства доказательства используются для множества задач, но даже полностью автоматические системы доказали ряд интересных и сложных теорем, включая по крайней мере одну, которая долгое время ускользала от математиков, а именно гипотезу Роббинса . [10] [11] Однако эти успехи случаются нерегулярно, и для решения сложных проблем обычно требуется опытный пользователь.
Другое различие иногда проводится между доказательством теорем и другими методами, когда процесс считается доказательством теоремы, если он состоит из традиционного доказательства, начиная с аксиом и производя новые шаги вывода с использованием правил вывода. Другие методы могут включать проверку модели , которая в простейшем случае включает в себя перебор многих возможных состояний (хотя фактическая реализация средств проверки моделей требует большой хитрости и не сводится просто к грубой силе).
Существуют гибридные системы доказательства теорем, в которых проверка модели используется в качестве правила вывода. Существуют также программы, которые были написаны для доказательства конкретной теоремы с (обычно неформальным) доказательством того, что если программа завершается с определенным результатом, то теорема верна. Хорошим примером этого было машинное доказательство теоремы о четырех цветах , которое было очень спорным как первое заявленное математическое доказательство, которое было по существу невозможно проверить людьми из-за огромного объема вычислений программы (такие доказательства называются непроверенными). -обследуемые доказательства ). Другой пример программного доказательства - это доказательство, которое показывает, что игру Connect Four всегда может выиграть первый игрок.
Промышленное использование
Коммерческое использование автоматического доказательства теорем в основном сосредоточено в разработке и проверке интегральных схем . После ошибки Pentium FDIV сложные модули с плавающей запятой современных микропроцессоров были разработаны с особой тщательностью. AMD , Intel и другие используют автоматическое доказательство теорем, чтобы убедиться, что деление и другие операции правильно реализованы в их процессорах.
Доказательство теорем первого порядка
В конце 1960-х годов агентства, финансирующие исследования в области автоматизированной дедукции, начали подчеркивать необходимость практического применения. Одной из первых плодотворных областей была проверка программ, при которой средства доказательства теорем первого порядка применялись к проблеме проверки правильности компьютерных программ на таких языках, как Паскаль, Ада и т. Д. Среди ранних систем проверки программ примечательным был Стэнфордский верификатор Паскаля. разработан Дэвидом Лакхэмом из Стэнфордского университета . Это было основано на Стэнфордский Резолюцию прувер также разработанном в Стэнфорд , используя Джон Алан Робинсон «s разрешение принципа. Это была первая автоматизированная система дедукции, демонстрирующая способность решать математические задачи, о которых было объявлено в Уведомлениях Американского математического общества до того, как решения были официально опубликованы. [ необходима цитата ]
Доказательство теорем первого порядка - одно из наиболее зрелых направлений автоматизированного доказательства теорем. Логика достаточно выразительна, чтобы можно было определять произвольные проблемы, часто достаточно естественным и интуитивно понятным способом. С другой стороны, он все еще является полуразрешимым, и был разработан ряд надежных и полных исчислений, позволяющих использовать полностью автоматизированные системы. [12] Более выразительные логики, такие как логики высшего порядка , позволяют удобно выражать более широкий круг проблем, чем логика первого порядка, но доказательство теорем для этих логик развито не так хорошо. [13] [14]
Контрольные точки, конкурсы и источники
Качество реализованных систем улучшилось благодаря существованию большой библиотеки стандартных примеров тестов - Библиотеки задач Thousands of Problems for Theorem Provers (TPTP) [15], а также ежегодного конкурса CADE ATP System Competition (CASC). конкуренция систем первого порядка для многих важных классов задач первого порядка.
Некоторые важные системы (все они выиграли по крайней мере одно соревнование CASC) перечислены ниже.
- E - это высокопроизводительное средство доказательства для полной логики первого порядка, но построенное на чисто эквациональном исчислении , первоначально разработанное в группе автоматизированных рассуждений Технического университета Мюнхена под руководством Вольфганга Бибеля , а теперь в Кооперативном государственном университете Баден-Вюртемберга. в Штутгарте .
- Otter , разработанный в Аргоннской национальной лаборатории , основан на разрешении первого порядка и парамодуляции . С тех пор Otter был заменен на Prover9 , который работает в паре с Mace4 .
- SETHEO - это высокопроизводительная система, основанная на исчислении целенаправленной модели исключения , первоначально разработанная командой под руководством Вольфганга Бибеля . E и SETHEO были объединены (с другими системами) в составном средстве доказательства теорем E-SETHEO.
- Вампир был первоначально разработан и реализован в Манчестерском университете Андреем Воронковым и Кристофом Ходером. Сейчас его разрабатывает растущая международная команда. Он регулярно побеждал в подразделении FOF (среди других подразделений) на соревнованиях CADE ATP System Competition с 2001 года.
- Waldmeister - это специализированная система для единично-эквациональной логики первого порядка, разработанная Арнимом Бухом и Томасом Хилленбрандом. Он выигрывал подразделение CASC UEQ четырнадцать лет подряд (1997–2010).
- SPASS - это программа для доказательства логических теорем первого порядка с равенством. Он разработан исследовательской группой «Автоматизация логики» Института компьютерных наук Макса Планка .
Музей средства доказательства теорем - это инициатива по сохранению источников систем доказательства теорем для будущего анализа, поскольку они являются важными культурными / научными артефактами. Он имеет источники многих из упомянутых выше систем.
Популярные техники
- Резолюция первого порядка с унификацией
- Исключение модели
- Метод аналитических таблиц
- Наложение и переписывание терминов
- Проверка модели
- Математическая индукция [16]
- Диаграммы двоичных решений
- DPLL
- Объединение высшего порядка
Программные системы
Имя | Тип лицензии | веб-сервис | Библиотека | Автономный | Последнее обновление ( формат ГГГГ-мм-дд ) |
---|---|---|---|---|---|
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 г., |
Свободное программное обеспечение
- Альт-Эрго
- Автомат
- CVC
- E
- GKC
- Машина Гёделя
- iProver
- IsaPlanner
- Устройство доказательства теорем КЭД [17]
- LeanCoP [18]
- Лев II
- LCF
- Приложение для браузера Logictools
- LoTREC [19]
- MetaPRL [20]
- Мицар
- NuPRL
- Парадокс
- Доказатель9
- Упрощать
- СПАРК (язык программирования)
- Двенадцать
- Z3 Доказательство теорем
Проприетарное программное обеспечение
- Acumen RuleManager (коммерческий продукт)
- АЛЛИГАТОР (CC BY-NC-SA 2.0 UK)
- КАРИН
- KIV (свободно доступен как плагин для Eclipse )
- Подключаемый модуль Prover (коммерческий тестовый двигатель)
- ProverBox
- Wolfram Mathematica [21]
- ResearchCyc
- Модульная арифметическая программа доказательства теорем спира
Смотрите также
- Переписка Карри – Ховарда
- Символьное вычисление
- Компьютерное доказательство
- Формальная проверка
- Логическое программирование
- Проверка доказательств
- Проверка модели
- Сложность доказательства
- Система компьютерной алгебры
- Программный анализ (информатика)
- Решение общих проблем
- Язык Metamath для формализованной математики
Заметки
- ^ Фреге, Готтлоб (1879). Begriffsschrift . Verlag Louis Neuert.
- ^ Фреге, Готтлоб (1884). Die Grundlagen der Arithmetik (PDF) . Бреслау: Вильгельм Кобнер. Архивировано из оригинального (PDF) 26 сентября 2007 года . Проверено 2 сентября 2012 .
- ^ Бертран Рассел; Альфред Норт Уайтхед (1910–1913). Принципы математики (1-е изд.). Издательство Кембриджского университета.
- ^ Бертран Рассел; Альфред Норт Уайтхед (1927). Принципы математики (2-е изд.). Издательство Кембриджского университета.
- ^ Эрбранд, Жак (1930). Исследования по теории демонстрации .
- ^ Пресбургер, 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.
- ^ а б в г Дэвис, Мартин (2001), «Ранняя история автоматизированного вывода» , Робинсон, Алан ; Воронков, Андрей (ред.), Справочник по автоматизированному мышлению , 1 , Elsevier)
- ^ Бибель, Вольфганг (2007). «Ранняя история и перспективы автоматизированного дедукции» (PDF) . Ki 2007 . LNAI. Спрингер (4667): 2–18 . Проверено 2 сентября 2012 года .
- ^ Гилмор, Пол (1960). «Процедура доказательства для теории квантификации: ее обоснование и реализация». Журнал исследований и разработок IBM . 4 : 28–35. DOI : 10.1147 / rd.41.0028 .
- ^ WW McCune (1997). «Решение проблемы Роббинса». Журнал автоматизированных рассуждений . 19 (3): 263–276. DOI : 10,1023 / A: 1005843212881 .
- ^ Джина Колата (10 декабря 1996 г.). «Доказательство компьютерной математики показывает силу рассуждений» . Нью-Йорк Таймс . Проверено 11 октября 2008 .
- ^ Ловленд, DW (1986). «Автоматическое доказательство теорем: отображение логики в ИИ» . Материалы международного симпозиума ACM SIGART по методологиям интеллектуальных систем - . Ноксвилл, штат Теннесси, США: ACM Press: 224. DOI : 10,1145 / 12808,12833 . ISBN 978-0-89791-206-8.
- ^ Кербер, Манфред. « Как доказать теоремы высшего порядка в логике первого порядка ». (1999).
- ^ Benzmüller, Christoph, et al. « LEO-II - кооперативная программа автоматического доказательства теорем для классической логики высшего порядка (описание системы) ». Международная совместная конференция по автоматическому мышлению. Шпрингер, Берлин, Гейдельберг, 2008 г.
- ^ Сатклифф, Джефф. «Библиотека задач TPTP для автоматизированного доказательства теорем» . Проверено 15 июля 2019 .
- ↑ Банди, Алан. Автоматизация доказательства математической индукцией . 1999 г.
- ^ Artosi, Альберто, Паола Каттабрига и Guido Governatori. « Кед: деонтический инструмент для доказательства теорем ». Одиннадцатая международная конференция по логическому программированию (ICLP'94). 1994 г.
- ^ Оттен, Йенс; Бибель, Вольфганг (2003). «LeanCoP: Lean, основанное на соединении доказательство теорем» . Журнал символических вычислений . 36 (1–2): 139–161. DOI : 10.1016 / S0747-7171 (03) 00037-3 .
- ^ дель Серро, Луис Фаринас и др. « Lotrec: универсальная программа для проверки модальных логик и логик описания ». Международная совместная конференция по автоматическому мышлению. Шпрингер, Берлин, Гейдельберг, 2001.
- ^ Хики, Джейсон и др. « MetaPRL - модульная логическая среда ». Международная конференция по доказательству теорем в логиках высокого порядка. Шпрингер, Берлин, Гейдельберг, 2003.
- ^ [1] Документация по системе Mathematica
Рекомендации
- Чин-Лян Чанг; Ричард Чар-Тунг Ли (1973). Символьная логика и механическое доказательство теорем . Академическая пресса .
- Ловленд, Дональд В. (1978). Автоматическое доказательство теорем: логическая основа. Фундаментальные исследования в области компьютерных наук Том 6 . Издательство Северной Голландии .
- Лакхэм, Дэвид (1990). Программирование со спецификациями: введение в Anna, язык для спецификации программ Ada . Тексты и монографии Springer-Verlag по информатике, 421 стр. ISBN 978-1461396871.
- Галлье, Жан Х. (1986). Логика для компьютерных наук: основы автоматического доказательства теорем . Издательство Harper & Row (доступно для бесплатной загрузки).
- Даффи, Дэвид А. (1991). Принципы автоматизированного доказательства теорем . Джон Вили и сыновья .
- Вос, Ларри; Овербек, Росс; Ласк, Юинг; Бойл, Джим (1992). Автоматизированное рассуждение: введение и приложения (2-е изд.). Макгроу – Хилл .
- Алан Робинсон; Андрей Воронков, ред. (2001). Справочник по автоматическому мышлению Том I и II . Elsevier и MIT Press .
- Фиттинг, Мелвин (1996). Логика первого порядка и автоматическое доказательство теорем (2-е изд.). Springer .
Внешние ссылки
- Список инструментов для доказательства теорем