Лекция
Привет, Вы узнаете о том , что такое автоматическое доказательство теорем, Разберем основные их виды и особенности использования. Еще будет много подробных примеров и описаний. Для того чтобы лучше понимать что такое автоматическое доказательство теорем , настоятельно рекомендую прочитать все из категории Моделирование и Моделирование систем.
Автоматизированное доказательство теорем (также известное как ATP или автоматизированная дедукция ) — это подраздел автоматизированных рассуждений и математической логики , связанный с доказательством математических теорем с помощью компьютерных программ . Автоматизация рассуждений над математическими доказательствами явилась важным стимулом для развития компьютерных наук .
автоматическое доказательство теорем (АДТ) — это область искусственного интеллекта и математики, которая занимается разработкой компьютерных программ или систем, способных автоматически генерировать формальные доказательства для математических теорем.
Целью АДТ является создание алгоритмов и методов, которые могут эффективно и надежно доказывать теоремы в различных математических областях, включая логику, алгебру, анализ, теорию чисел и другие.
Автоматическое доказательство теорем обычно основано на формализации математических теорий и правил вывода в компьютерной системе. Затем система применяет логические рассуждения, алгоритмы проверки и преобразования высказываний, чтобы автоматически строить доказательства для заданных утверждений или опровергать их.
Возможные методы, используемые в автоматическом доказательстве теорем, включают резолюцию, прямые методы, методы таблиц истинности, механизмы вывода с помощью искусственных нейронных сетей и другие. Также используются формальные языки и системы верификации для формализации и проверки доказательств.
Хотя корни формализованной логики восходят к Аристотелю , в конце 19-го и начале 20-го веков развилась современная логика и формализованная математика. Begriffsschrift Фреге (1879) представил как полное исчисление высказываний , так и то , что по существу является современной логикой предикатов . Его «Основы арифметики» , опубликованные в 1884 году, выражали (частично) математику в формальной логике. Этот подход был продолжен Расселом и Уайтхедом в их влиятельных Principia Mathematica , впервые опубликованных в 1910–1913 гг и с исправленным вторым изданием в 1927 году. Рассел и Уайтхед думали, что они могут вывести всю математическую истину, используя аксиомы и правила вывода формальной логики, в принципе открывая процесс для автоматизации. В 1920 году Торальф Сколем упростил предыдущий результат Леопольда Левенгейма , что привело к теореме Левенгейма-Скулема , а в 1930 году — к понятию вселенной Гербранда и интерпретации Гербранда , которая допускала (не)выполнимость формул первого порядка (и, следовательно, справедливостьтеоремы) сводится к (потенциально бесконечному количеству) пропозициональных проблем выполнимости .
В 1929 году Мойжеш Пресбургер показал, что теория натуральных чисел со сложением и равенством (теперь называемая арифметикой Пресбургера в его честь) разрешима , и дал алгоритм, который мог определить, является ли данное предложение в языке истинным или ложным. Однако вскоре после этого положительного результата Курт Гедель опубликовал «О формально неразрешимых утверждениях принципов математики и родственных систем» (1931 г.), показав, что в любой достаточно сильной аксиоматической системе есть истинные утверждения, которые не могут быть доказаны в системе . Эта тема получила дальнейшее развитие в 1930-х годах Алонсо Черчем иАлан Тьюринг , который с одной стороны дал два независимых, но эквивалентных определения вычислимости , а с другой привел конкретные примеры для неразрешимых вопросов.
Вскоре после Второй мировой войны появились первые компьютеры общего назначения. В 1954 году Мартин Дэвис запрограммировал алгоритм Пресбургера для компьютера с электронными лампами JOHNNIAC в Институте перспективных исследований в Принстоне, штат Нью-Джерси. По словам Дэвиса, «его великим триумфом было доказать, что сумма двух четных чисел четна». Более амбициозной была Logic Theory Machine в 1956 году, система дедукции для пропозициональной логики Principia Mathematica , разработанная Алленом Ньюэллом , Гербертом А. Саймоном и Дж. К. Шоу.. Также работающая на JOHNNIAC, Logic Theory Machine построила доказательства из небольшого набора пропозициональных аксиом и трех правил вывода: modus ponens , (пропозициональная) подстановка переменных и замена формул их определением. Система использовала эвристическое руководство и сумела доказать 38 из первых 52 теорем Principia .
«Эвристический» подход Логической Теоретико-Машины пытался подражать человеческим математикам и не мог гарантировать, что доказательство может быть найдено для каждой действительной теоремы даже в принципе. Об этом говорит сайт https://intellect.icu . Напротив, другие, более систематические алгоритмы достигли, по крайней мере теоретически, полноты для логики первого порядка. Первоначальные подходы основывались на результатах Хербранда и Сколема для преобразования формулы первого порядка в последовательно увеличивающиеся наборы пропозициональных формул путем создания экземпляров переменных с терминами из вселенной Хербранда . Затем пропозициональные формулы можно было бы проверить на невыполнимость, используя ряд методов. Программа Гилмора использовала преобразование в дизъюнктивную нормальную форму , форму, в которой выполнимость формулы очевидна
В зависимости от лежащей в основе логики проблема определения правильности формулы варьируется от тривиальной до невозможной. Для частого случая логики высказываний проблема разрешима, но ко-NP-полная , и, следовательно, считается, что для общих задач доказательства существуют только алгоритмы с экспоненциальным временем. Для исчисления предикатов первого порядка теорема Геделя о полноте утверждает , что теоремы (доказуемые утверждения) являются в точности логически верными правильно сформированными формулами , поэтому идентификация действительных формул рекурсивно перечислима : при неограниченных ресурсах любая действительная формула может быть в конечном итоге доказана. Однако недопустимые формулы (те, которые невытекающие из данной теории), не всегда могут быть признаны.
Сказанное относится к теориям первого порядка, таким как арифметика Пеано . Однако для конкретной модели, которая может быть описана теорией первого порядка, некоторые утверждения могут быть верными, но неразрешимыми в теории, используемой для описания модели. Например, по теореме Геделя о неполноте, мы знаем, что любая теория, чьи собственные аксиомы верны для натуральных чисел, не может доказать истинность всех утверждений первого порядка для натуральных чисел, даже если список собственных аксиом можно перечислить бесконечно. Из этого следует, что автоматический доказатель теорем не остановится при поиске доказательства именно тогда, когда исследуемое утверждение неразрешимо в используемой теории, даже если оно истинно в интересующей модели. Несмотря на этот теоретический предел, на практике средства доказательства теорем могут решить множество сложных задач, даже в моделях, которые не полностью описываются какой-либо теорией первого порядка (например, целыми числами).
Более простой, но связанной с этим проблемой является проверка доказательства , когда существующее доказательство теоремы признается действительным. Для этого обычно требуется, чтобы каждый отдельный шаг доказательства мог быть проверен примитивной рекурсивной функцией или программой, и, следовательно, проблема всегда разрешима.
Поскольку доказательства, генерируемые автоматическими средствами доказательства теорем, обычно очень велики, проблема сжатия доказательств имеет решающее значение, и были разработаны различные методы, направленные на то, чтобы сделать вывод средства доказательства меньшим и, следовательно, более понятным и проверяемым.
Помощникам проверки требуется, чтобы пользователь-человек давал подсказки системе. В зависимости от степени автоматизации, прувер можно по существу свести к средству проверки доказательств, при этом пользователь предоставляет доказательство формальным способом, или важные задачи проверки могут выполняться автоматически. Интерактивные доказывающие используются для самых разных задач, но даже полностью автоматические системы доказали ряд интересных и сложных теорем, в том числе по крайней мере одну, которая долгое время ускользала от математиков-людей, а именно гипотезу Роббинса . [10] [11] Однако эти успехи единичны, и для работы над сложными задачами обычно требуется опытный пользователь.
Другое различие иногда проводится между доказательством теорем и другими методами, когда процесс считается доказательством теорем, если он состоит из традиционного доказательства, начиная с аксиом и производя новые шаги вывода с использованием правил вывода. Другие методы могут включать проверку модели , которая в простейшем случае включает в себя перебор многих возможных состояний методом грубой силы (хотя фактическая реализация средств проверки модели требует большого ума и не сводится к простому грубому перебору).
Существуют гибридные системы доказательства теорем, которые используют проверку модели в качестве правила вывода. Существуют также программы, которые были написаны для доказательства конкретной теоремы с (обычно неформальным) доказательством того, что если программа завершается с определенным результатом, то теорема верна. Хорошим примером этого было машинное доказательство теоремы о четырех красках , которое было очень спорным, поскольку первое заявленное математическое доказательство было практически невозможно проверить людьми из-за огромного объема вычислений программы (такие доказательства называются неподтвержденными) . -опровержимые доказательства ). Еще один пример доказательства с помощью программы — тот, который показывает, что в игре « Соедини четыре» всегда может выиграть первый игрок.
Коммерческое использование автоматизированного доказательства теорем в основном сосредоточено в разработке и проверке интегральных схем . После ошибки Pentium FDIV сложные блоки с плавающей запятой современных микропроцессоров разрабатывались с особой тщательностью. AMD , Intel и другие используют автоматическое доказательство теорем, чтобы убедиться, что деление и другие операции правильно реализованы в их процессорах.
Автоматическое доказательство теорем имеет широкий спектр применений, включая верификацию программ и аппаратных средств, проверку правильности математических утверждений, анализ систем и протоколов безопасности, разработку формальных языков и др.
Однако, автоматическое доказательство теорем стало объектом активного исследования, и не все математические теоремы могут быть полностью автоматически доказаны в настоящее время. Многие задачи требуют вмешательства человека, интуиции и креативности для поиска и формулирования доказательств.
В конце 1960-х годов агентства, финансирующие исследования в области автоматической дедукции, начали подчеркивать необходимость их практического применения. Одной из первых плодотворных областей была верификация программ , в которой средства доказательства теорем первого порядка применялись к проблеме проверки правильности компьютерных программ на таких языках, как Паскаль, Ада и т. д. Среди первых систем верификации программ примечательной была Stanford Pascal Verifier. разработан Дэвидом Лакхэмом из Стэнфордского университета . [ 12] [13] [14] Это было основано на Stanford Resolution Prover, также разработанном в Стэнфорде с использованием разрешения Джона Алана Робинсона .принцип. Это была первая автоматизированная система вывода, которая продемонстрировала способность решать математические задачи, о которых было объявлено в Уведомлениях Американского математического общества до того, как решения были официально опубликованы. [ нужна ссылка ]
Доказательство теорем первого порядка — одно из наиболее зрелых направлений автоматизированного доказательства теорем. Логика достаточно выразительна, чтобы можно было описать произвольные проблемы, часто достаточно естественным и интуитивным способом. С другой стороны, он все еще полуразрешим, и был разработан ряд надежных и полных исчислений, позволяющих полностью автоматизировать системы. [15] Более выразительные логики, такие как логика высшего порядка , позволяют удобно выражать более широкий спектр проблем, чем логика первого порядка, но доказательство теорем для этих логик развито хуже. [16] [17]
Качество реализованных систем улучшилось благодаря существованию большой библиотеки стандартных тестовых примеров — Библиотека задач «Тысячи задач для доказательств теорем» (TPTP) [18] — а также ежегодному конкурсу CADE ATP System Competition (CASC). конкуренция систем первого порядка для многих важных классов задач первого порядка.
Некоторые важные системы (все они выиграли хотя бы в одном соревновательном дивизионе CASC) перечислены ниже.
Музей доказательства теорем является инициативой по сохранению источников систем доказательства теорем для будущего анализа, поскольку они являются важными культурными/научными артефактами. Он имеет источники многих систем, упомянутых выше.
Исследование, описанное в статье про автоматическое доказательство теорем, подчеркивает ее значимость в современном мире. Надеюсь, что теперь ты понял что такое автоматическое доказательство теорем и для чего все это нужно, а если не понял, или есть замечания, то не стесняйся, пиши или спрашивай в комментариях, с удовольствием отвечу. Для того чтобы глубже понять настоятельно рекомендую изучить всю информацию из категории Моделирование и Моделирование систем
Комментарии
Оставить комментарий
Моделирование и Моделирование систем
Термины: Моделирование и Моделирование систем