3. Метод резолюций

   1. Конъюнктивная нормальная форма

Любую формулу, как логики высказываний, так и логики предикатов можно преобразовать в эквивалентную ей формулу, имеющую вид “нормальной” (или “канонической”) формы. В этом отношении представляют интерес понятия дизъюнкт и конъюнктивная нормальная форма (КНФ).

Дизъюнктом называется дизъюнкция конечного числа литер (литера – это атом P или его отрицание  P).

Дизъюнкт эквивалентен дизъюнкции (а не конъюнкции) его элементов. Пустой дизъюнкт – единственный невыполнимый дизъюнкт, который обозначается символом .

Конъюнктивной нормальной формой (КНФ) называется конъюнкция конечного числа дизъюнктов.

Рассмотрим этапы получения КНФ:

1. Исключаются связки эквивалентности и импликации в соответствии с правилами:

A  B  ( A  B ) & ( B  A )

A  B   A  B

2. Переименовываются (если необходимо) связанные переменные таким образом, чтобы никакая переменная не имела бы одновременно свободных и связанных вхождений. Это условие требуется не только для рассматриваемой формулы, но также для всех её подформул.

3. Удаляются те квантификации, область действия которых не содержит вхождений квантифицированной переменной.

 z R ( a, x, y ) преобразуется в R ( a, x, y )

4. Все вхождения отрицания преобразуются в отрицания, стоящие непосредственно перед атомами, в соответствии со следующими правилами:

  x A   x  A

  x A   x  A

 (  A )  A  закон двойного отрицания

 ( A  B )   A &  B  1-ый закон де Моргана

 ( A & B )   A   B  2-ой закон де Моргана

5. Необходимое число раз применяются правила преобразования, выведенные из законов дистрибутивности:

A  ( B & C )  ( A  B ) & ( A  C )

A & ( B  C )  ( A & B )  ( A & C )

6. Все квантификации перемещаются в начало формулы. Для этого используется соответствующий набор правил преобразования.

Описание задач и алгоритмов в терминах дизъюнктов составляют основу логического программирования вообще и языка Пролог в частности.

2. Дизъюнкт Хорна

Рассмотрим фрагмент программы:

брат ( фёдор, иван ).

отец ( иван, пётр ).

дядя ( U, N ) :-

брат ( U, B ),

отец ( B, N ).

Правило дядя означает:

Если брат ( U, B ) и отец ( B, N ), то дядя ( U, N )



брат ( U, B ) & отец ( B, N )  дядя ( U, N )

Заменим предикаты формальными символами:

B₁ & B₂  A

Получим КНФ:

B₁ & B₂  A   ( B₁ & B₂ )  A   B₁   B₂  A

Обобщим полученный результат.

Любое правило имеет вид: A  B₁, B₂, …, B_n

что эквивалентно A   B₁   B₂  …   B_n

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

Дизъюнкт, содержащий не более одного положительного литерала, называется хорновским дизъюнктом (или дизъюнктом Хорна).

Дизъюнкт Хорна выражает некоторое правило: негативные литеры соответствуют посылкам (которые представлены соответствующими утверждениями), а позитивная литера представляет заключение.

Унитарный позитивный дизъюнкт представляет некоторый факт, то есть заключение, независящее ни от каких посылок.

Задача состоит в том, что надо проверить какую-то формулу (называемую целью), логически выведенную из множества фактов и правил.