stringtranslate.com

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

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

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

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

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

Ранние года

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

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

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

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

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

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

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

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

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

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

Приложения

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

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

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

Журналы

Сообщества

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

  1. ^ Дефурно, Жиль и Николя Пельтье. «Аналогия и похищение в автоматизированной дедукции». ИДЖКАИ (1). 1997.
  2. ^ Джон Л. Поллок [ нужна полная цитата ]
  3. ^ К. Хейлз, Томас «Формальное доказательство», Питтсбургский университет. Проверено 19 октября 2010 г.
  4. ^ ab «Автоматизированный вывод (AD)», [Природа проекта PRL] . Проверено 19 октября 2010 г.
  5. ^ Мартин Дэвис (1983). «Предыстория и ранняя история автоматизированной дедукции». В Йорге Зикманне; Дж. Райтсон (ред.). Автоматизация рассуждений (1) - Классические статьи по вычислительной логике 1957–1966 гг. Гейдельберг: Спрингер. стр. 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, номер документа : 10.1007/BF00263446, S2CID  14824949
  11. ^ Гонтье, Г.; и другие. (2013), «Машинно-проверенное доказательство теоремы нечетного порядка» (PDF) , в Blazy, S .; Полен-Мёринг, К.; Пичарди, Д. (ред.), Интерактивное доказательство теорем , Конспект лекций по информатике, том. 7998, стр. 163–179, CiteSeerX 10.1.1.651.7964 , doi : 10.1007/978-3-642-39634-2_14, ISBN  978-3-642-39633-5, S2CID  1855636
  12. ^ Хойле, Марин Дж. Х .; Куллманн, Оливер; Марек, Виктор В. (2016). «Решение и проверка булевой задачи о тройках Пифагора с помощью Cube and Conquer». Теория и приложения тестирования выполнимости – SAT 2016 . Конспекты лекций по информатике. Том. 9710. стр. 228–245. arXiv : 1605.00723 . дои : 10.1007/978-3-319-40970-2_15. ISBN 978-3-319-40969-6. S2CID  7912943.
  13. ^ Средство доказательства теоремы Бойера-Мура, получено 23 октября 2010 г.
  14. ^ Бойер, Роберт С. и Мур, Дж. Стротер и Пассмор, Грант Олни. Архив PLTP . Получено 27 июля 2023 г.
  15. ^ Харрисон, Джон ХОЛ Лайт: обзор . Проверено 23 октября 2010 г.
  16. ^ Введение в Coq . Проверено 23 октября 2010 г.
  17. ^ Автоматизированное рассуждение , Стэнфордская энциклопедия . Проверено 10 октября 2010 г.

Внешние ссылки