Программирование на языке Пролог для искусственного интеллекта

символов. Например, утверждение, записанное в виде формулы

p  v  ~ p

и означающее 'p или не p', верно всегда, независимо от смысла утверждения p.

Мы будем использовать в качестве операторов следующие символы:

~     отрицание, читается как  'не'

&    конъюнкцию, читается как  'и'

v    дизъюнкцию, читается как  'или'

=>  импликацию, читается как  'следует'

Согласно правилам предпочтения операторов, оператор 'не' связывает утверждения сильнее, чем 'и', 'или' и 'следует'.

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

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

(а  =>  b) & (b  =>  с) => (а  =>  с)

Смысл этой формулы таков: если из а следует b и из b следует с, то из а следует с.

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

(р₁  v  p₂  v  …)  &  (q₁  v  q₂  v  …)

      &  (r₁  v  r₂  v  …)  &  …

Здесь р_i, q_i, ri — элементарные утверждения или их отрицания. Конъюнктивная нормальная форма есть конъюнкция членов, называемых дизъюнктами, например (p₁ v p₂ v …) — это дизъюнкт.

Любую пропозициональную формулу нетрудно преобразовать в такую форму. В нашем случае это делается следующим образом. У нас есть исходная формула

(а  =>  b)  &  (b  =>  с)  =>  (а  =>  с)

Ее отрицание имеет вид

~((а  =>  b) & (b  =>  с) => (а  =>  с))

Для преобразования этой формулы в конъюнктивную нормальную форму можно использовать следующие известные правила:

(1) x => у  эквивалентно  ~x v у

(2) ~(x v y)  эквивалентно ~x & ~у

(3) ~ (x & у)  эквивалентно  ~x v ~у

(4) ~ (~x)  эквивалентно  x

Применяя правило 1, получаем

~(~((a  =>  b)  &  (b  =>  с))  v  (а  =>  с))

Далее, правила 2 и 4 дают

(а  =>  b)  &  (b  =>  с)  &  ~ (а  =>  с)

Трижды применив правило 1, получаем

(~а  v  b)  &  (~b  v  с)  &  ~(~а  v  с)

И наконец, после применения правила 2 получаем искомую конъюнктивную нормальную форму

(~а  v  b)  &  (~b  v  с)  &  а  &  ~с

состоящую из четырех дизъюнктов. Теперь можно приступить к резолюционному процессу.

Элементарный шаг резолюции выполняется всегда, когда имеется два дизъюнкта, в одном из которых встретилось элементарное утверждение p, а в другом — ~p. Пусть этими двумя дизъюнктами будут

p v Y  и  ~p v Z

Шаг резолюции порождает третий дизъюнкт:

Y  v  Z

Нетрудно показать, что этот дизъюнкт логически следует из тех двух дизъюнктов, из которых он получен. Таким образом, добавив выражение (Y v Z) к нашей исходной формуле, мы не изменим ее истинности. Резолюционный процесс порождает новые дизъюнкты. Появление 'пустого дизъюнкта' (обычно записываемого как 'nil') сигнализирует о противоречии. Действительно, пустой дизъюнкт nil порождается двумя дизъюнктами вида

x  и  ~x

которые явно противоречат друг другу.

Рис. 16.6. Доказательство теоремы (а=>b)& (b=>с)=>(a=>с) методом резолюции. Верхняя строка — отрицание теоремы в конъюнктивной нормальной форме. Пустой дизъюнкт внизу сигнализирует, что отрицание теоремы противоречиво.

На рис. 16.6 показан процесс применения резолюций, начинающийся с отрицания нашей предполагаемой теоремы и заканчивающийся пустым дизъюнктом.

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

если

 существуют два таких дизъюнкта C1 и C2, что P является (дизъюнктивным) подвыражением C1, а ~P — подвыражением C2