3. Резолюция и логический вывод в Прологе

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

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

Таким образом, принцип резолюции заключается в том, чтобы исходя из фактов, правил и отрицания цели, получить противоречие (пустой дизъюнкт).

Логика работы компьютера состоит в том, что он путём подбора контрпримеров пытается опровергнуть отрицание. Основанием для такого рода “умозаключения” служит закон противоречия, который гласит: “Не могут быть одновременно истинны утверждение и его отрицание”.

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

цель отец ( X, пётр )

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

нет такого X, где бы встречалось «X отец петра»

Затем компьютер находит факт отец ( иван, пётр ), и этот факт является контрпримером для указанного отрицания, а следовательно решение X = иван становится ответом-опровержением.

Логический вывод в Прологе состоит из отдельных шагов вывода, на каждом из которых применяется резолюция.

Резолюцию проще всего ввести, рассмотрев сначала одну из наиболее простых её форм. Допустим, что имеются отрицание и импликация:

отрицание B₁: A

импликация B₂: A  B

В результате одного шага вывода из B₁ и B₂ получается новое предложение

B: B

Пояснение: есть два дизъюнкта A и B  A; так как формула A  A   общезначима, то она может быть опущена.

Предложения B₁ и B₂ на шаге вывода называются родительскими предложениями, а предложение B называется резольвентой, которая получается в результате применения резолюции к родительским предложениям.

Например,

B₁: Змея НЕ млекопитающее. % 1-ое родительское предложение

B₂: ЕСЛИ кто-то кормит детёныша молоком,

ТО этот кто-то млекопитающее. % 2-ое родительское предложение

B: Змея НЕ кормит детёныша молоком. % резолюция

Рассмотрим теперь ещё более простой случай, в котором B₁ является отрицанием, а B₂ является фактом:

отрицание B₁: A

факт B₂: A

Получаем противоречие A и A

резольвента B: 

Проиллюстрируем принцип резолюции на примере. Пусть необходимо доказать формулу: если из A следует B и из B следует C, то из A следует C.

Исходная формула: ( A  B ) & ( B  C )  ( A  C )

Её отрицание:  ( ( A  B ) & ( B  C )  ( A  C ) )

Вспомним формулы:

P  Q   P  Q % 1

 ( P  Q )   P &  Q % 2

 (  P )  P % 3

Получим КНФ для отрицания:

 ( ( A  B ) & ( B  C )  ( A  C ) ) % 1

 (  ( ( A  B ) & ( B  C ) )  ( A  C ) )

 (  ( ( A  B ) & ( B  C ) )  ( A  C ) ) % 2, 3

( A  B ) & ( B  C ) &  ( A  C )

( A  B ) & ( B  C ) &  ( A  C ) % 1 (3 раза)

(  A  B ) & (  B  C ) &  (  A  C )

(  A  B ) & (  B  C ) &  (  A  C ) % 2

(  A  B ) & (  B  C ) & A &  C

КНФ состоит из четырёх дизъюнктов. Теперь будем выполнять резолюционный процесс.

Элементарный шаг резолюции выполняется всегда, когда имеется два дизъюнкта, в одном из которых встретилось элементарное утверждение, а в другом – его отрицание. Например, есть два дизъюнкта: P  Y и  P  Z. Шаг резолюции порождает третий дизъюнкт: Y  Z. При добавлении выражения ( Y  Z ) к формуле её истинность не меняется. Резолюционный процесс порождает новые дизъюнкты. Появление пустого дизъюнкта сигнализирует о противоречии, что в свою очередь означает завершение процесса.

 A  B		 B  C		A	 C
	 A  C
			C
				

На основании вышеизложенного можно сформулировать два вывода:

1. Резолюция соответствует стандартному правилу вывода modus tollens, суть которого выражается следующим образом:

допуская, что не А и А если В,

выводим не В.

2. Последовательно применяя резолюцию к родительским предложениям выводим в качестве резольвенты пустое отрицание:

допуская, что не А и А,

выводим противоречие.

Пример. Для того чтобы понять назначение выводов в контексте решения задачи, рассмотрим простой пример, связанный с логикой понятий давать и получать.

Пусть предикат даёт ( X, Y, Z ) означает

“X даёт Y некоторому объекту Z”.

Другой предикат получает ( Z, Y ) означает

“некоторый объект Z получает Y”.

Допустим, что некоторые знания об этих отношениях выражаются двумя предложениями:

В₂: получает ( вы, сила )  даёт ( логика, сила, вы )

В₃: даёт ( логика, сила, вы )

Задача, которую нужно решить, состоит в том, чтобы ответить на вопрос “получаете ли вы силу”?

В логическом программировании такой вопрос представляется в виде отрицания:

В₁:  получает ( вы, сила )

Система должна опровергнуть это отрицание при помощи других предложений. Опровержение отрицания происходит путём демонстрации того, что его допущение ведёт к противоречию.

1 шаг вывода: Система применит правило резолюции к В₁ и В₂ и

получит резольвенту В:  даёт ( логика, сила, вы )

2 шаг вывода: Система применит резолюцию к В и В₃ и

получит противоречие: В’: 

Для доказательства противоречивости входных предложений В₁, В₂, В₃ оказалось достаточно, таким образом, двух шагов вывода. Следовательно, ответом для исходной задачи является да.

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

S₁:  (A₁, …, A_k, …, A_n)

S₂: A_k  B₁, …, B_m

, где 1  k  n

Здесь некоторый предикат A_k из отрицания S₁ совпадает с заключением из импликации S₂.

В этой ситуации шаг вывода заменяет A_k в S₁ на посылки из S₂, и в качестве резольвенты получает отрицание

S:  ( A₁, …, A_k-1, B₁, …, B_m, A_k+1, …, A_n )

Детали вывода, которого достаточно для выполнения общей резолюции сверху вниз, можно суммировать следующим образом:

Шаг 1. Во избежание путаницы переименовываются переменные, чтобы отрицание S₁ и импликация S₂ не содержали общих переменных; при этом смысл родительских предложений никак не меняется.

Шаг 2. В отрицании S₁ выбирается предикат, у которого имя предиката совпадает с именем заключения в импликации S₂. Если такого предиката нет, то шаг вывода становится невозможным.

Шаг 3. Для выбранного предиката из S₁ и выбранного заключения из S₂ ищется наиболее общий унификатор Θ. Если унификатора не существует, то шаг вывода невозможен. Вспомним, что в логике предикатов используются переменные, которые связываются в процессе унификации. Конкретное значение, полученное переменной в результате подстановки, называют унификатором.

Шаг 4. Выбранный в S₁ предикат заменяется посылками из импликации S₂ (если S₂ является фактом, он просто вычёркивается). В результате получается новое (возможно пустое) отрицание.

Шаг 5. Унификатор Θ применяется к новому отрицанию. В результате получается резольвента S предложений S₁ и S₂.