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

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

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

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

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

Ранние годы

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

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

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

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

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

Теоретик логики (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.Сельберг -Erds
2005Джордан КриваяHOL LightХейлзThomassen
2005Фиксированная точка БрауэраHOL LightХаррисонKuhn
2006Муха 1ИзабельБауэр-НипковХейлз
2007Остаток КошиHOL LightХаррисонКлассический
2008Простое числоHOL LightХаррисонАналитическое доказательство
2012Фейт-ТомпсонCoqGonthier et al.[11]Бендер, Глауберман и Петерфальви
2016Проблема логических троек ПифагораФормализована как СИДЕЛHeule et al.[12]Никто

Системы доказательства

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

Приложения

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

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

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

Журналы

Сообщества

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

  1. ^ Дефурно, Жиль и Николя Пельтье. "Аналогия и абдукция в автоматизированной дедукции. »IJCAI (1). 1997.
  2. ^ Джон Л. Поллок
  3. ^ К. Хейлз, Томас «Формальное доказательство», Университет Питтсбурга. Проверено 19 октября 2010 г.
  4. ^ а б «Автоматическое удержание (AD)», [Природа проекта PRL]. Проверено 19 октября 2010 г.
  5. ^ Мартин Дэвис (1983). «Предыстория и ранняя история автоматизированного дедукции». В Йорге Зикманне; Г. Райтсон (ред.). Автоматизация рассуждений (1) - Классические статьи по вычислительной логике 1957–1966 гг.. Гейдельберг: Springer. С. 1–28. ISBN  978-3-642-81954-4. Здесь: стр.15
  6. ^ "Принципы математики", в Стэндфордский Университет. Проверено 19 октября 2010 г.
  7. ^ "Теоретик логики и его дети". Проверено 18 октября 2010 г.
  8. ^ Шанкар, Натараджан Маленькие двигатели доказательства, Лаборатория компьютерных наук, SRI International. Проверено 19 октября 2010 г.
  9. ^ Шанкар, Н. (1994), Метаматематика, машины и доказательство Гёделя, Кембридж, Великобритания: Издательство Кембриджского университета, ISBN  9780521585330
  10. ^ Руссинофф, Дэвид М. (1992), "Механическое доказательство квадратичной взаимности", J. Autom. Причина., 8 (1): 3–21, Дои:10.1007 / BF00263446
  11. ^ Gonthier, G .; и другие. (2013), "Машинно-проверенное доказательство теоремы о нечетном порядке" (PDF), в Blazy, S .; Paulin-Mohring, C .; Пичарди, Д. (ред.), Интерактивное доказательство теорем, Конспект лекций по информатике, 7998, стр. 163–179, Дои:10.1007/978-3-642-39634-2_14, ISBN  978-3-642-39633-5
  12. ^ Heule, Marijn J. H .; Куллманн, Оливер; Марек, Виктор В. (2016). «Решение и проверка булевой проблемы троек Пифагора с помощью куба и завоевания». Теория и приложения тестирования выполнимости - SAT 2016. Конспект лекций по информатике. 9710. С. 228–245. arXiv:1605.00723. Дои: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 г.

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