Автоматизированное рассуждение - Automated reasoning


Из Википедии, свободной энциклопедии

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

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

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

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

Ранние года

Развитие формальной логики играет большую роль в области автоматизированного мышления, которое само по себе привело к развитию искусственного интеллекта . Формальное доказательство является доказательством , в котором каждый логический вывод был проверен назад к основным аксиомам математики. Все промежуточные логические шаги поставляются без исключения. Никакое обращение не сделано к интуиции, даже если перевод от интуиции к логике является обычным делом. Таким образом, формальное доказательство менее интуитивное и менее восприимчиво к логическим ошибкам.

Некоторые считают Летнюю встречу Cornell 1957, в котором приняли участие большое количество логиков и компьютерных ученых, как происхождение автоматизированных рассуждений или автоматизированной дедукции . Другие говорят , что это началось до того, что с 1955 Logic теоретиком программы Ньюэлл, Шоу и Саймон, или Мартина Дэвиса 1954 года осуществления процедуры принятия Пресбургера в (который доказал , что сумма двух четных чисел четно). Автоматизированное рассуждение, хотя значительная и популярная область исследований, прошла через « AI зиму » в восьмидесятых и начале девяностых лет. Поле впоследствии возродилась, однако. Например, в 2005 году Microsoft начала использовать технологию проверки во многих своих внутренних проектов и планирует включить логическую спецификацию и проверку языка в их версии Визуальный C. 2012

Значительный вклад

Principia Mathematica является важной вехой работы в формальной логике , написанной Альфред Норт Уайтхед и Бертран Рассел . Principia Mathematica - также означает Принципы математики - была написана с целью получить все или некоторые из математических выражений , в терминах символической логики . Principia Mathematica первоначально был опубликован в трех томах в 1910, 1912 и 1913.

Логика Теоретик (LT) была первая программаразработанная в 1956 году Аллен Ньюэлл , Клифф Шоу и Герберт А. Саймон в «имитируют человеческие рассуждения» в доказательстве теоремы и было продемонстрировано на пятьдесят две теоремы из главы второй Principia Mathematica, доказав тридцать -eight из них. В дополнении к доказательству теоремы, программа нашла доказательства для одной из теоремкоторый был более элегантнымчемусловии Уайтхед и Рассел. После неудачной попытки публикации их результатов, Ньюэлл, Шоу и Герберт сообщили в их публикации в 1958 г. Следующий Эдванс исследования операций :

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

Примеры формальных доказательств

Год теорема Доказательство системы Formalizer Традиционный Proof
1986 Во-первых Неполнота Бойер-Мур Шанкар Гедель
1990 Квадратное Взаимность Бойер-Мур Russinoff Эйзенштейн
1996 Фундаментализм из Исчисления HOL Light Харрисон Хенстока
2000 Фундаментализм алгебры Мицар Milewski Brynski
2000 Фундаментализм алгебры Coq Geuvers и др. Кнезер
2004 Четыре цвета Coq Гонтье Робертсон и соавт.
2004 Простое число Isabelle Avigad и др. Сельберг - Erdős
2005 Иордания Curve HOL Light Hales Thomassen
2005 Брауэр Фиксированная точка HOL Light Харрисон Кун
2006 точечка 1 Isabelle BAUER-Нипкова Hales
2007 Коши остаток HOL Light Харрисон классическая
2008 Простое число HOL Light Харрисон аналитическое доказательство
2012 Фейт-Томпсон Coq Гонтье и др. Бендеры, Глауберман и Peterfalvi
2016 Логический Пифагор тройки проблемы Формализованное в SAT Heule и др. никто

Proof системы

Бойер-Мур теорема Prover (NQTHM)
Дизайн NQTHM под влиянием Джона Маккарти и Вуди Бледсо. Создано в 1971 году в Эдинбурге, Шотландия, это был полностью автоматической теорема доказывающей построен с использованием Pure Lisp . Основные аспекты NQTHM были:
  1. использование Lisp в качестве рабочей логики.
  2. опора на принцип определения для общих рекурсивных функций.
  3. широкое использование перезаписи и «символической оценки».
  4. индукционная эвристический на основе провала символической оценки.
HOL Light
Написанная в OCaml , HOL Light разработан , чтобы иметь простую и чистую логическую основу и лаконичные реализации. Это, по существу , еще одно доказательство помощник для классической высшей логики порядка.
Coq
Разработанный во Франции, Coq является еще одним доказательством автоматизирован помощник, который может автоматически извлекать исполняемые программы из спецификаций, либо как Objective CAML или Haskell исходный код. Свойства, программа и доказательства оформляются в том же языке под названием Исчисление Индуктивного конструкция (CIC).

Приложения

Автоматизированное рассуждение было наиболее часто используется для построения автоматизированных прувер теоремы. Часто, однако, теорема испытатели требуют некоторого человеческого руководства , чтобы быть эффективными и поэтому более обычно квалифицируются как помощники доказательства . В некоторых случаях такие испытатели придумали новые подходы к доказательству теоремы. Логика Теоретик является хорошим примером этого. Программа придумала доказательство одной из теорем в Principia Mathematica , который был более эффективным (требует меньше шагов) , чем доказательства , представленных Уайтхед и Рассел. Автоматизированные программы рассуждения применяются для решения растущего числа проблем формальной логики, математики и информатики, логического программирования , программного обеспечения и аппаратных средств контроля, схемотехнике , и многие другие. TPTP (Сатклифф и Suttner 1998) представляет собой библиотеку таких проблем, обновляется на регулярной основе. Существует также конкуренция среди автоматизированных испытателей теоремы регулярно проводимых на КАДЕ конференции (Pelletier, Сатклифф и Suttner 2002); проблемы для конкуренции выбирается из библиотеки TPTP.

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

Конференции и семинары

Журналы

Сообщества

Рекомендации

  1. ^ Джон Л. Поллок
  2. ^ С. Hales, Томас «Формальное доказательство» , Университет Питтсбурга. Проверено 2010-10-19
  3. ^ Б «Автоматизированный Вычет (AD)» , [Природа ПРЛ проекта] . Проверено 2010-10-19
  4. ^ Мартин Дэвис, «предыстория и ранняя история автоматизированной дедукции» в автоматизации рассуждений, ред. Siekmann и Райтсон, т. 1, 1-28 при р. 15
  5. ^ "Principia Mathematica" , в Стэнфордском университете . Источник 2010-10-19
  6. ^ «Логика Теоретик и ее дети» . Источник 2010-10-18
  7. ^ Шанкар, Натараян Маленькие Двигатели Proof , Computer Science Laboratory, SRI International . Источник 2010-10-19
  8. ^ Шанкар, N. (1994), Метаматематика, Машина и доказательство Гёделя , Кембридж, Великобритания: Cambridge University Press, ISBN  9780521585330
  9. ^ Russinoff, Дэвид М. (1992), «Механическое Доказательство квадратичной Взаимности», Ж. Авт. Причина. , 8 (1): 3-21, DOI : 10.1007 / BF00263446
  10. ^ Гонтие, G .; и другие. (2013), «машинно-Проверено Доказательство теоремы нечетного порядка», в Блази, S .; Паулин-Möhring, С .; Pichardie Д., Интерактивная теорема Доказывая , Lecture Notes в области компьютерных наук, 7998 , стр 163-179,. Дои : 10.1007 / 978-3-642-39634-2_14 , ISBN  978-3-642-39633-5
  11. ^ Heule, Marijn JH; Кульман, Оливер; Marek, Victor W. (2016). «Решение и проверка Логическое Пифагора троек Проблема с помощью кубика и властвуй». Теория и применение ВЫПОЛНИМОСТЬ тестирования - SAT 2016 года . Lecture Notes в области компьютерных наук. 9710 . стр. 228-245. Arxiv : 1605,00723 . DOI : 10.1007 / 978-3-319-40970-2_15 . ISBN  978-3-319-40969-6 .
  12. ^ Boyer- Мур теорема Prover . Проверено 2010-10-23
  13. ^ Харрисон, Джон HOL свет: обзор . Источник 2010-10-23
  14. ^ Введение в Coq . Источник 2010-10-23
  15. ^ Автоматизированная Рассуждая , Stanford Encyclopedia . Источник 2010-10-10

внешняя ссылка