Введение
Подполе информатики и логики В информатике, в частности в представлении знаний и рассуждениях и металогике, область автоматизированных рассуждений посвящена пониманию различных аспектов рассуждений. Изучение автоматического рассуждения помогает создавать компьютерные программы, которые позволяют компьютерам рассуждать полностью или почти полностью автоматически. Хотя автоматическое рассуждение считается подполем искусственного интеллекта, оно также имеет связи с теоретической информатикой и философией. Наиболее развитыми подобластями автоматизированного рассуждения являются автоматизированное доказательство теоремы (и менее автоматизированное, но более прагматичное подполе интерактивного доказательства теоремы) и автоматизированная проверка доказательств (считается гарантированным правильным рассуждением при фиксированных предположениях). Обширная работа также была проведена в рассуждениях по аналогии с использованием индукции и абдукции. Другие важные темы включают рассуждения в условиях неопределенности и немонотонные рассуждения. Важной частью поля неопределенности является аргументация, где дополнительные ограничения минимальности и согласованности применяются в дополнение к более стандартному автоматическому вычету. Система ОСКАР Джона Поллока является примером автоматизированной системы аргументации, которая является более специфичной, чем просто автоматизированный теорема проверка. Инструменты и методы автоматизированного рассуждения включают классическую логику и калькули, нечеткую логику, байесовское выводы, рассуждения с максимальной энтропией и многие менее формальные методы ad hoc.
In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub field of artificial intelligence, it also has connections with theoretical computer science and philosophy. The most developed subareas of automated reasoning are automated theorem proving (and the less automated but more pragmatic subfield of interactive theorem proving) and automated proof checking (viewed as guaranteed correct reasoning under fixed assumptions). Extensive work has also been done in reasoning by analogy using induction and abduction. Other important topics include reasoning under uncertainty and non monotonic reasoning. An important part of the uncertainty field is that of argumentation, where further constraints of minimality and consistency are applied on top of the more standard automated deduction. John Pollock's OSCAR system is an example of an automated argumentation system that is more specific than being just an automated theorem prover. Tools and techniques of automated reasoning include the classical logics and calculi, fuzzy logic, Bayesian inference, reasoning with maximal entropy and many less formal ad hoc techniques.
Приложения
Автоматизированное рассуждение чаще всего используется для создания автоматизированных доказателей теорем. Однако часто для доказательства теоремы требуется некоторое руководство человека, чтобы быть эффективным, и поэтому более обычно квалифицируются как помощники доказательства. В некоторых случаях такие доказывающие придумывают новые подходы к доказательству теоремы. Логический теоретик - хороший пример этого. Программа придумала доказательство одной из теорем Principia Mathematica, которое было более эффективным (требующим меньшего количества шагов), чем доказательство, предоставленное Уайтхедом и Расселом. Программы автоматического рассуждения применяются для решения растущего числа проблем в формальной логике, математике и информатике, логическом программировании, проверке программного и аппаратного обеспечения, проектировании схем и многих других. TPTP (Sutcliffe and Suttner 1998) - это библиотека таких проблем, которая регулярно обновляется. Также регулярно проводится конкурс среди автоматизированных проверяющих теоремы на конференции CADE (Pelletier, Sutcliffe and Suttner 2002); задачи для конкурса выбираются из библиотеки TPTP.