Правило вывода

Правило вывода — это формальное предписание или алгоритм, позволяющий на основании одного или нескольких утверждений (посылок) получить новое утверждение (заключение). Правила вывода являются центральным понятием в логике, математике, информатике и теории искусственного интеллекта, где они используются для построения доказательств, проверки корректности рассуждений и реализации механизмов логического вывода.

Основные понятия

Правило вывода обычно записывается в виде схемы, где над чертой перечислены посылки, под чертой — заключение. Например, классическое правило modus ponens (лат. «правило отделения»):

\[ \frac{A, \quad A \rightarrow B}{B} \]

Здесь \(A\) и \(A \rightarrow B\) — посылки, \(B\) — заключение. Если утверждения \(A\) и «если \(A\), то \(B\)» истинны, то истинным будет и \(B\).

Важнейшие свойства правил вывода:

• Корректность (сохраняемость истинности): если все посылки истинны, то заключение также должно быть истинным.
• Полнота: набор правил вывода позволяет получить все логические следствия из заданных посылок.
• Разрешимость: существует ли алгоритм, который за конечное число шагов определяет, применимо ли правило к данным посылкам.

Классификация правил вывода

Правила вывода можно классифицировать по нескольким основаниям.

По типу логики

• Классическая логика высказываний: правила modus ponens, modus tollens, введение и удаление конъюнкции, дизъюнкции, импликации, отрицания.
• Логика предикатов первого порядка: дополнительно включают правила кванторов (введение и удаление кванторов всеобщности и существования).
• Нечёткая логика: правила вывода оперируют нечёткой истинностью (например, правило композиционного вывода Заде).
• Модальные логики: правила, учитывающие модальности (необходимость, возможность, знание, вера).
• Немонотонные логики: правила, допускающие отзыв ранее полученных заключений при поступлении новой информации.

По структуре

• Прямые правила: из посылок непосредственно получают заключение (modus ponens).
• Обратные правила: из заключения и одной из посылок выводят другую посылку (modus tollens).
• Правила резолюции: универсальное правило для автоматического доказательства теорем, основанное на принципе резолюции Робинсона.

По числу посылок

• Однопосылочные: например, правило введения двойного отрицания (\(A \vdash \neg\neg A\)).
• Двухпосылочные: modus ponens, modus tollens, правило цепного заключения (гипотетический силлогизм).
• Многопосылочные: правило резолюции, правило введения конъюнкции (из \(A\) и \(B\) выводится \(A \land B\)).

Примеры классических правил вывода

Modus ponens (лат. «правило отделения»)

\[ \frac{A, \quad A \rightarrow B}{B} \] Пример: если «идёт дождь» (A) и «если идёт дождь, то земля мокрая» (A → B), то «земля мокрая» (B).

Modus tollens (лат. «правило отрицания»)

\[ \frac{A \rightarrow B, \quad \neg B}{\neg A} \] Пример: если «если идёт дождь, то земля мокрая» и «земля не мокрая», то «дождь не идёт».

Гипотетический силлогизм (правило цепного заключения)

\[ \frac{A \rightarrow B, \quad B \rightarrow C}{A \rightarrow C} \] Пример: если «если число делится на 4, то оно чётное» и «если число чётное, то оно делится на 2», то «если число делится на 4, то оно делится на 2».

Правило резолюции

\[ \frac{A \lor B, \quad \neg A \lor C}{B \lor C} \] Это правило лежит в основе метода резолюций, широко используемого в автоматическом доказательстве теорем и логическом программировании (например, в языке Пролог).

Применение правил вывода

В математике и логике

Правила вывода являются основой формальных систем, в которых аксиомы и правила вывода образуют исчисление. Например, в исчислении высказываний Гильберта используются всего несколько правил (modus ponens и подстановка), а все остальные теоремы выводятся из аксиом.

В информатике и искусственном интеллекте

• Экспертные системы: правила вывода (часто в форме «если — то») используются для моделирования знаний эксперта и принятия решений.
• Логическое программирование: в языке Пролог программа состоит из фактов и правил, а механизм вывода (резолюция) автоматически находит ответы на запросы.
• Базы знаний и онтологии: правила вывода позволяют извлекать неявные знания из явно заданных фактов (например, если «Сократ — человек» и «все люди смертны», то «Сократ смертен»).
• Автоматическое доказательство теорем: системы типа Coq, Isabelle, Lean используют правила вывода для формальной верификации программ и математических доказательств.

В когнитивной науке и психологии

Правила вывода рассматриваются как модели человеческого рассуждения. Исследования показывают, что люди часто допускают ошибки при применении правил (например, путают modus ponens и modus tollens), что связано с особенностями когнитивной обработки информации.

Критика и ограничения

• Немонотонность: классические правила вывода монотонны — добавление новых посылок не может отменить ранее полученные заключения. В реальном мире рассуждения часто немонотонны (например, при рассуждениях по умолчанию).
• Проблема фреймов: в системах искусственного интеллекта применение правил вывода к большому числу фактов может привести к комбинаторному взрыву.
• Ограниченность формализма: не все виды человеческих рассуждений (индуктивные, абдуктивные, аналоговые) сводятся к дедуктивным правилам вывода.
• Зависимость от аксиоматики: корректность правил вывода зависит от выбранной аксиоматической системы; в разных логиках одни и те же правила могут быть некорректными.

Интересные факты

• Первые формальные правила вывода были сформулированы Аристотелем в «Органоне» (силлогизмы). Однако современное понятие правила вывода как части формальной системы сложилось в работах Готлоба Фреге, Бертрана Рассела и Альфреда Тарского.
• В 1931 году Курт Гёдель доказал теоремы о неполноте, которые показали, что для достаточно выразительных формальных систем (например, арифметики Пеано) не существует полного и непротиворечивого набора правил вывода, позволяющего доказать все истинные утверждения.
• Правило резолюции, открытое Джоном Аланом Робинсоном в 1965 году, стало основой для языка Пролог и многих систем автоматического доказательства теорем.

Источники

• Мендельсон Э. Введение в математическую логику. — М.: Наука, 1976.
• Гиндикин С. Г. Алгебра логики в задачах. — М.: Наука, 1972.
• Рассел С., Норвиг П. Искусственный интеллект: современный подход. — М.: Вильямс, 2006.
• Клини С. К. Математическая логика. — М.: Мир, 1973.
• Тарский А. Введение в логику и методологию дедуктивных наук. — М.: Издательство иностранной литературы, 1948.