Автоматизированное рассуждение
Автоматизированное мышление - это область компьютерных наук (включающая представление знаний и рассуждение) и металогика, посвященная пониманию различных аспектов рассуждения. Изучение автоматизированного мышления помогает создавать компьютерные программы, которые позволяют компьютерам рассуждать полностью или почти полностью автоматически. Хотя автоматизированное мышление считается одной из областей искусственного интеллекта, оно также связано с теоретической информатикой и философией.
Наиболее развитыми подразделами автоматизированного рассуждения являются автоматизированное доказательство теоремы (и менее автоматизированное, но более прагматичное подполе интерактивного доказательства теоремы) и автоматизированная проверка доказательств (рассматриваемая как гарантированное правильное рассуждение при фиксированных допущениях). кроме того, была проделана обширная работа по рассуждению по аналогии с использованием индукции и похищения .]
Другие важные темы включают рассуждения в условиях неопределенности и немонотонные рассуждения. Важной частью поля неопределенности является область аргументации,где дополнительные ограничения минимальности и согласованности применяются поверх более стандартного автоматизированного вывода. Система Оскара Джона Поллока[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.
См. также[править]
- Автоматизированное машинное обучение (AutoML)
- Автоматическое доказательство теоремы
- Система рассуждений
- Семантический рассуждатель
- Анализ программ (информатика)
- Применение искусственного интеллекта
- Контур искусственного интеллекта
- Казуистика * аргументация на основе конкретных случаев
- Похищающее рассуждение
- Механизм вывода
- Рассуждения здравого смысла
Конференции и семинары
- Международная совместная конференция по автоматизированному рассуждению (IJCAR)
- Конференция по автоматизированному вычету (CADE)
- Международная конференция по автоматизированному рассуждению с аналитическими таблицами и связанными с ними методами
Журналы
Сообщества
Пруф[править]
web.archive.org/web/20090310081227/http://www.csc.liv.ac.uk/~konev/iwil2008/