Автоматизированное рассуждение
В информатике , в частности в представлении знаний, рассуждениях и металогике , область автоматизированных рассуждений посвящена пониманию различных аспектов рассуждения . Изучение автоматизированных рассуждений помогает создавать компьютерные программы , которые позволяют компьютерам рассуждать полностью или почти полностью автоматически. Хотя автоматизированное мышление считается подобластью искусственного интеллекта , оно также имеет связь с теоретической информатикой и философией .
Наиболее развитыми подобластями автоматизированного рассуждения являются автоматическое доказательство теорем (и менее автоматизированное, но более прагматичное подразделение интерактивного доказательства теорем ) и автоматическая проверка доказательств (рассматриваемая как гарантированно правильное рассуждение при фиксированных предположениях). [ нужна ссылка ] Обширная работа была также проделана в рассуждениях по аналогии с использованием индукции и абдукции . [ 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 ]
Примеры формальных доказательств
Год Теорема Система доказательств Формализатор Традиционное доказательство 1986 Первая незавершенность Бойер-Мур Шанкар [ 9 ] Гёдель 1990 Квадратичная взаимность Бойер-Мур Руссинофф [ 10 ] Эйзенштейн 1996 Основы исчисления ХОЛ Лайт Харрисон Хенсток 2000 Основы алгебры Плотник Милевский Брынский 2000 Основы алгебры Кок Геверс и др. Колени 2004 Четыре цвета Кок Гонтье Робертсон и др. 2004 Простое число Изабель Авигад и др. Сельберг - Лес 2005 Джордан Кривая ХОЛ Лайт Хейлз Томассен 2005 Фиксированная точка Брауэра ХОЛ Лайт Харрисон Кун 2006 Характеристики полета 1 Изабель Бауэр-Нипков Хейлз 2007 Остаток Коши ХОЛ Лайт Харрисон Классический 2008 Простое число ХОЛ Лайт Харрисон Аналитическое доказательство 2012 Факт-Томпсон Кок Гонтье и др. [ 11 ] Бендер, Глауберман и Петерфальви 2016 Булева задача о тройках Пифагора Формализовано как SAT Хойле и др. [ 12 ] Никто
Системы доказательств
[ редактировать ]- Средство доказательства теорем Бойера-Мура (NQTHM)
- На дизайн NQTHM повлияли Джон Маккарти и Вуди Бледсо. Созданная в 1971 году в Эдинбурге, Шотландия, это была полностью автоматическая программа для доказательства теорем, созданная с использованием Pure Lisp . Основными аспектами NQTHM были:
- ХОЛ Лайт
- , написанный на OCaml , HOL Light имеет простую и понятную логическую основу и лаконичную реализацию. По сути, это еще один помощник в доказательстве классической логики высшего порядка. [ 15 ]
- Кок
- — еще один автоматизированный помощник проверки, разработанный во Франции Coq , который может автоматически извлекать исполняемые программы из спецификаций в виде исходного кода Objective CAML или Haskell . Свойства, программы и доказательства формализуются на том же языке, который называется исчислением индуктивных конструкций (CIC). [ 16 ]
Приложения
[ редактировать ]Автоматизированное рассуждение чаще всего использовалось для создания автоматизированных средств доказательства теорем. Однако зачастую для того, чтобы доказать свою эффективность, специалистам по доказательству теорем требуется некоторое человеческое руководство, и поэтому их чаще называют помощниками по доказательству . В некоторых случаях такие доказыватели придумали новые подходы к доказательству теоремы. Теоретик логики является хорошим примером этого. Программа предложила доказательство одной из теорем Principia Mathematica , которое было более эффективным (требующим меньше шагов), чем доказательство, предоставленное Уайтхедом и Расселом. Программы автоматического рассуждения применяются для решения растущего числа задач в формальной логике, математике и информатике, логическом программировании , проверке программного и аппаратного обеспечения, проектировании схем и многих других. TPTP (Сатклифф и Саттнер , 1998) представляет собой библиотеку таких задач, которая регулярно обновляется. регулярно проводятся соревнования среди автоматизированных средств доказательства теорем Также на конференции CADE (Пеллетье, Сатклифф и Саттнер, 2002); задачи для конкурса выбраны из библиотеки ТПТП. [ 17 ]
См. также
[ редактировать ]- Автоматизированное машинное обучение (AutoML)
- Автоматизированное доказательство теорем
- Система рассуждений
- Семантическое рассуждение
- Программный анализ (информатика)
- Приложения искусственного интеллекта
- Очерк искусственного интеллекта
- Казуистика • Рассуждение на основе прецедентов
- Абдуктивное рассуждение
- Механизм вывода
- Рассуждения здравого смысла
Конференции и семинары
[ редактировать ]- Международная совместная конференция по автоматическому рассуждению (IJCAR)
- Конференция по автоматизированному дедукции (CADE)
- Международная конференция по автоматизированному рассуждению с помощью аналитических таблиц и связанным с ними методам
Журналы
[ редактировать ]Сообщества
[ редактировать ]Ссылки
[ редактировать ]- ^ Дефурно, Жиль и Николя Пельтье. « Аналогия и похищение в автоматизированной дедукции ». ИДЖКАИ (1). 1997.
- ^ Джон Л. Поллок [ нужна полная цитата ]
- ^ К. Хейлз, Томас «Формальное доказательство» , Питтсбургский университет. Проверено 19 октября 2010 г.
- ^ Jump up to: а б «Автоматизированный вывод (AD)» , [Природа проекта PRL] . Проверено 19 октября 2010 г.
- ^ Мартин Дэвис (1983). «Предыстория и ранняя история автоматизированной дедукции». В Йорге Зикманне; Г. Райтсон (ред.). Автоматизация рассуждений (1) — Классические статьи по вычислительной логике, 1957–1966 гг . Гейдельберг: Спрингер. стр. 1–28. ISBN 978-3-642-81954-4 . Здесь: стр.15
- ^ «Principia Mathematica» в Стэнфордском университете . Проверено 19 октября 2010 г.
- ^ «Теоретик логики и его дети» . Проверено 18 октября 2010 г.
- ^ Шанкар, Натараджан «Маленькие машины доказательства» , Лаборатория компьютерных наук, SRI International . Проверено 19 октября 2010 г.
- ^ Шанкар, Н. (1994), Метаматематика, машины и доказательство Гёделя , Кембридж, Великобритания: Cambridge University Press, ISBN 9780521585330
- ^ Руссинофф, Дэвид М. (1992), «Механическое доказательство квадратичной взаимности», J. Autom. Причина. , 8 (1): 3–21, doi : 10.1007/BF00263446 , S2CID 14824949
- ^ Гонтье, Г.; и др. (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
- ^ Хойле, Марин Дж. Х .; Куллманн, Оливер; Марек, Виктор В. (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 .
- ^ Средство доказательства теоремы Бойера-Мура, получено 23 октября 2010 г.
- ^ Бойер, Роберт С. и Мур, Дж. Стротер и Пассмор, Грант Олни. Архив PLTP . Получено 27 июля 2023 г.
- ^ Харрисон, Джон ХОЛ Лайт: обзор . Проверено 23 октября 2010 г.
- ^ Введение в Coq . Проверено 23 октября 2010 г.
- ^ Автоматизированное рассуждение , Стэнфордская энциклопедия . Проверено 10 октября 2010 г.