В информатике , в частности в представлении знаний, рассуждениях и металогике , область автоматизированного рассуждения посвящена пониманию различных аспектов рассуждения . Изучение автоматизированных рассуждений помогает создавать компьютерные программы , которые позволяют компьютерам рассуждать полностью или почти полностью автоматически. Хотя автоматизированное рассуждение считается подобластью искусственного интеллекта , оно также имеет связь с теоретической информатикой и философией .
Наиболее развитыми подобластями автоматизированного рассуждения являются автоматическое доказательство теорем (и менее автоматизированное, но более прагматичное подразделение интерактивного доказательства теорем ) и автоматическая проверка доказательств (рассматриваемая как гарантированно правильное рассуждение при фиксированных предположениях). [ нужна цитация ] Обширная работа также была проделана в рассуждениях по аналогии с использованием индукции и абдукции . [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 года « Следующий прогресс в исследовании операций »:
Примеры формальных доказательств
Автоматизированное рассуждение чаще всего использовалось для создания автоматизированных средств доказательства теорем. Однако зачастую для того, чтобы доказать свою эффективность, специалистам по доказательству теорем требуется некоторое человеческое руководство, и поэтому их чаще называют помощниками по доказательству . В некоторых случаях такие доказыватели придумали новые подходы к доказательству теоремы. Теоретик логики является хорошим примером этого. Программа предложила доказательство одной из теорем Principia Mathematica , которое было более эффективным (требующим меньше шагов), чем доказательство, предоставленное Уайтхедом и Расселом. Программы автоматического рассуждения применяются для решения растущего числа задач в формальной логике, математике и информатике, логическом программировании , проверке программного и аппаратного обеспечения, проектировании схем и многих других. TPTP (Сатклифф и Саттнер , 1998) представляет собой библиотеку таких задач, которая регулярно обновляется. Также на конференции CADE регулярно проводятся соревнования среди автоматизированных средств доказательства теорем (Пеллетье, Сатклифф и Саттнер, 2002); задачи для конкурса выбраны из библиотеки ТПТП. [17]