Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

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

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

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

Ранние годы [ править ]

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

Некоторые считают, что корнельское летнее собрание 1957 года, собравшее многих логиков и компьютерных ученых, начало автоматизированных рассуждений или автоматизированной дедукции . [4] Другие говорят, что это началось до этого с программы теоретиков логики 1955 года Ньюэлла, Шоу и Саймона или с реализации Мартином Дэвисом 1954 года процедуры принятия решений Пресбургера (которая доказала, что сумма двух четных чисел четна). [5]

Автоматические рассуждения, хотя и являлись важной и популярной областью исследований, пережили « зиму искусственного интеллекта » в восьмидесятых и начале девяностых годов. Однако впоследствии это поле возродилось. Например, в 2005 году Microsoft начала использовать технологию проверки во многих своих внутренних проектах и ​​планирует включить логическую спецификацию и язык проверки в свою версию Visual C 2012 года [4].

Значительный вклад [ править ]

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

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

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

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

ГодТеоремаСистема доказательствФормализаторТрадиционное доказательство
1986 г.Первая неполнотаБойер-МурШанкар [9]Гёдель
1990 г.Квадратичная взаимностьБойер-МурРуссинофф [10]Эйзенштейн
1996 г.Основы исчисленияHOL LightХаррисонHenstock
2000 г.Основы алгебрыМицарМилевскиБрынский
2000 г.Основы алгебрыCoqGeuvers et al.Кнезер
2004 г.Четыре цветаCoqГонтьеРобертсон и др.
2004 г.Простое числоИзабельAvigad et al.Сельберг - Эрдёш
2005 г.Кривая ДжорданаHOL LightХейлзThomassen
2005 г.Фиксированная точка БрауэраHOL LightХаррисонKuhn
2006 г.Муха 1ИзабельБауэр-НипковХейлз
2007 г.Остаток КошиHOL LightХаррисонКлассический
2008 г.Простое числоHOL LightХаррисонАналитическое доказательство
2012 г.Фейт-ТомпсонCoqGonthier et al. [11]Бендер, Глауберман и Петерфальви
2016 г.Проблема логических троек ПифагораФормализована как SATHeule et al. [12]Никто

Системы доказательства [ править ]

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

Приложения [ править ]

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

См. Также [ править ]

  • Автоматизированное машинное обучение (AutoML)
  • Автоматическое доказательство теорем
  • Система рассуждений
  • Семантический рассуждающий
  • Программный анализ (информатика)
  • Приложения искусственного интеллекта
  • Схема искусственного интеллекта
  • Казуистика • Рассуждения на основе прецедентов
  • Абдуктивное рассуждение
  • Механизм логического вывода
  • Здравый смысл

Конференции и семинары [ править ]

  • Международная совместная конференция по автоматизированному мышлению (IJCAR)
  • Конференция по автоматическому вычету (CADE)
  • Международная конференция по автоматизированному мышлению с аналитическими таблицами и родственными методами

Журналы [ править ]

  • Журнал автоматизированных рассуждений

Сообщества [ править ]

  • Ассоциация автоматизированного мышления (AAR)

Ссылки [ править ]

  1. ^ Дефурно, Жиль и Николя Пельтье. « Аналогия и абдукция в автоматизированной дедукции ». IJCAI (1). 1997 г.
  2. ^ Джон Л. Поллок
  3. ^ К. Хейлз, Томас «Формальное доказательство» , Университет Питтсбурга. Проверено 19 октября 2010 г.
  4. ^ a b «Автоматическое удержание (AD)» , [Природа проекта PRL] . Проверено 19 октября 2010 г.
  5. ^ Мартин Дэвис (1983). «Предыстория и ранняя история автоматизированного дедукции». В Йорге Зикманне; Г. Райтсон (ред.). Автоматизация рассуждений (1) - Классические статьи по вычислительной логике 1957–1966 . Гейдельберг: Springer. С. 1–28. ISBN 978-3-642-81954-4. Здесь: стр.15
  6. ^ "Principia Mathematica" в Стэнфордском университете . Проверено 19 октября 2010 г.
  7. ^ "Теоретик логики и его дети" . Проверено 18 октября 2010 г.
  8. ^ Шанкар, Натараджан Маленькие двигатели доказательства , Лаборатория компьютерных наук, SRI International . Проверено 19 октября 2010 г.
  9. ^ Шанкар, Н. (1994), Метаматематика, машины и доказательство Гёделя , Кембридж, Великобритания: Cambridge University Press, ISBN 9780521585330
  10. ^ Руссинофф, Дэвид М. (1992), "Механическое доказательство квадратичной взаимности", J. Autom. Причина. , 8 (1): 3-21, DOI : 10.1007 / BF00263446
  11. ^ Gonthier, G .; и другие. (2013), «Доказательство теоремы о нечетном порядке с машинной проверкой» (PDF) , в Blazy, S .; Paulin-Mohring, C .; Pichardie, Д. (ред.), Интерактивная теорема доказав , Lecture Notes в области компьютерных наук, 7998 , стр 163-179,. Дои : 10.1007 / 978-3-642-39634-2_14 , ISBN  978-3-642-39633-5
  12. ^ Heule, Marijn JH ; Куллманн, Оливер; Марек, Виктор В. (2016). «Решение и проверка булевой проблемы троек Пифагора с помощью Cube-and-Conquer». Теория и приложения проверки выполнимости - SAT 2016 . Конспект лекций по информатике. 9710 . С. 228–245. arXiv : 1605.00723 . DOI : 10.1007 / 978-3-319-40970-2_15 . ISBN 978-3-319-40969-6.
  13. ^ Инструмент доказательства теорем Бойера-Мура . Проверено 23 октября 2010 г.
  14. ^ Харрисон, Джон HOL Light: обзор . Проверено 23 октября 2010 г.
  15. ^ Введение в Coq . Проверено 23 октября 2010 г.
  16. ^ Автоматизированное рассуждение , Стэнфордская энциклопедия . Проверено 10 октября 2010 г.

Внешние ссылки [ править ]

  • Международный семинар по реализации логики
  • Серия семинаров по эмпирически успешным темам автоматизированного мышления