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

Материал из wikixw
(разн.) ← Предыдущая версия | Текущая версия (разн.) | Следующая версия → (разн.)
Перейти к навигации Перейти к поиску

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

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

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

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

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

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

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

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

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

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

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

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

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

Год Теорема Система Доказательства Формализатор Традиционное Доказательство
1986 Первая Неполнота Бойер-Мур Шанкар Gödel
1990 Квадратичная Взаимность Бойер-Мур Русинов Eisenstein
1996 Фундаментальное-исчисление Хол свет Харрисон Хенсток
2000 Фундаментальная-Алгебра Мизар Милевский Брынский
2000 Фундаментальная-Алгебра Coq Geuvers et al. Кнесер
2004 Четыре Цвета Coq Гонтье Робертсон и др.
2004 Простое Число Isabelle Авигад и др. Selberg-Erdős
2005 Кривая Джордана Хол свет Хейлс Томассен
2005 Брауэр Фиксированная Точка Хол свет Харрисон Kuhn
2006 Мухоловка 1 Isabelle Бауэр-Нипков Хейлс
2007 Остаток Коши Хол свет Харрисон Классический
2008 Простое Число Хол свет Харрисон Аналитическое доказательство
2012 Feit-Thompson Coq Гонтье и др. Бендер, Глауберман и Петерфальви
2016 Булева задача о пифагорейских тройках Формализовано как СБ Heule et al. Нет

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

Доказательство теоремы Бойера-Мура (NQTHM)

  • На дизайн NQTHM оказали влияние Джон Маккарти и Вуди Бледсо. Начатое в 1971 году в Эдинбурге, Шотландия, Это было полностью автоматическое доказательство теоремы, построенное с использованием чистого Лиспа. Основными аспектами NQTHM были::
  • использование Lisp в качестве рабочей логики.
  • опора на принцип определения для полных рекурсивных функций.
  • широкое использование рерайтинга и"символической оценки".
  • эвристика индукции основана на провале символической оценки.

Хол свет

  • Написанный на OCaml, HOL Light спроектирован так, чтобы иметь простую и чистую логическую основу и лаконичную реализацию. Это, по существу, еще один помощник доказательства для классической логики высшего порядка.]

Coq

  • Разработанный во Франции, Coq является еще одним автоматизированным помощником доказательства, который может автоматически извлекать исполняемые программы из спецификаций, как объективный CAML или исходный код Haskell. Свойства, программы и доказательства формализуются на том же языке, который называется исчислением индуктивных конструкций (CIC).]

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

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

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

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

Журналы

Сообщества

Пруф[править]

web.archive.org/web/20090310081227/http://www.csc.liv.ac.uk/~konev/iwil2008/

Источник — https://wikixw.ru/index.php?title=Автоматизированное_рассуждение&oldid=23845