Математическое введение в декларативное программирование. Зюзысов В.М. - 36 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

Составители: 

Рубрика: 

6.4 Конъюнктивная нормальная форма
Литерал – это элементарная формула или отрицание элементарной формулы.
Дизъюнкт – это литерал или дизъюнкция конечного числа литералов.
Конъюнктивная нормальная форма – это формула, которая являются дизъюнктом или
конъюнкцией конечного числа дизъюнктов.
Теорема 9. Для любой формулы A, не содержащей кванторы, существует формула
B, являющаяся конъюнктивной нормальной формой (КНФ), и B логически эквивалентна
A.
Доказательство. Укажем алгоритм построения формулы B.
Исключаем связки эквивалентности и импликации по правилам: •
•
•
•
•
•
•
X~Y = (X⊃Y)&(Y⊃X);
X⊃Y = ¬X∨Y.
Протаскивание отрицаний. Преобразуем все вхождения отрицания в стоящие
непосредственно перед элементарными подформулами в соответствии со сле-
дующими правилами:
¬¬X = X;
¬(X∨Y) = ¬X&¬Y;
¬(X&Y) = ¬X∨¬Y.
Преобразуем полученную формулу, используя правило дистрибутивности ∨ от-
носительно &.
Пример. Приведем к КНФ формулу (X&Y)~(¬X&Z).
После первого этапа получаем
(X&Y)~(¬X&Z) = (X&Y ⊃ ¬X&Z) & (¬X&Z ⊃ X&Y) =
(¬(X&Y) ∨ (¬X&Z)) & (¬(¬X&Z) ∨ (X&Y)).
После второго этапа получаем
(¬(X&Y) ∨ (¬X&Z)) & (¬(¬X&Z) ∨ (X&Y)) = ((¬X∨¬Y) ∨ (¬X&Z)) & ((¬¬X∨¬Z) ∨ (X&Y))
= ((¬X∨¬Y) ∨ (¬X&Z)) & ((X∨¬Z) ∨ (X&Y)).
После третьего этапа получаем
((¬X∨¬Y) ∨ (¬X&Z)) & ((X∨¬Z) ∨ (X&Y)) =
(((¬X∨¬Y) ∨ ¬X) & ((¬X∨¬Y) ∨ Z)) & ((X∨¬Z) ∨ (X&Y)) =
(((¬X∨¬Y) ∨ ¬X) & ((¬X∨¬Y) ∨ Z)) & (((X∨¬Z) ∨ X) & ((X∨¬Z) ∨ Y)).
Используя идемпотентность и ассоциативность связок, упрощаем результат:
(¬X∨¬Y) & (¬X∨¬Y ∨Z) & (X∨¬Z)&(X∨¬Z∨Y).
Заметим, что в силу ассоциативности операций & и ∨, как бы мы не расставляли
скобки в выражениях A
1
&A
2
&…&A
n
и A
1
∨A
2
∨…∨A
n
(n>2), всегда будем приходить к ло-
гически эквивалентным формулам. Кроме того, КНФ не являются однозначно определен-
ным. Формула может иметь несколько равносильных друг другу КНФ.
6.5 Сведение к дизъюнктам
Метод резолюций работает с дизъюнктами. Любая формула A исчисления предика-
тов может быть преобразована в множество дизъюнктов следующим образом (здесь знак
→ используется для обозначения способа преобразования формул).
1. Приводим к предваренной форме. См. алгоритм в доказательстве теоремы 7. Получаем
формулу A
1
логически эквивалентную формуле A.
2. Проводим сколемизацию формулы A
1
и получаем формулу A
2
. По теореме 8 формулы
A
1
и A
2
одновременно выполнимы или невыполнимы.
3. Элиминация кванторов всеобщности. Выполняем преобразования вида: ∀x P(x) →
P(x). Это преобразование не является логически эквивалентным, но формула
∀xP(x)⊃P(x) является логически общезначимой. После третьего этапа получаем фор-
36

Страницы