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

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

Формула Q
1
x
1
... Q
n
x
n
A, где символ Q
i
означает либо ∀, либо ∃, x
i
и x
j
различны для
i ≠ j и A − не содержит кванторов, называется формулой в предваренной нормальной фор-
ме. (Сюда включается и случай n=0, когда вообще нет никаких кванторов.)
Без ограничения общности можно потребовать, чтобы квантифицированы могли
быть только переменные, имеющие свободное вхождение. Действительно, по правилам
интерпретации если формула A не содержит вхождений переменной x, то формулы A, ∃xA
и ∀xA имеют одно и то же значение истинности при всех интерпретациях.
Интерес к предваренным формам связан со следующей теоремой, справедливой
для всякой теории первого порядка,
Теорема 7. Существует алгоритм, преобразующий всякую формулу A к такой фор-
муле B в предваренной нормальной форме, что A=B.
Доказательство. Алгоритм получения предваренной формулы очень прост. Этапы
таковы:
Исключить связки эквивалентности и импликации по правилам: •
•
•
•
•
•
A~B ≡ (A⊃B)&(B⊃A) ≡ (A&B) ∨ (¬A&¬B);
A⊃B ≡ ¬A¤B ≡ ¬ (A&¬B).
Переименовать (если необходимо) связанные переменные таким образом, что-
бы никакая переменная не имела бы одновременно свободных и связанных
вхождений. Это условие требуется не только для рассматриваемой формулы, но
также для всех ее подформул.
Разделение связанных переменных. Логически эквивалентное преобразование:
Q
1
x A(...Q
2
x B(...x...)...) = Q
1
x A(...Q
2
y B(...y...)...), где Q
1
и Q
2
− любые кванторы и
y − любая переменная, не входящая в формулу B(...x...).
Удалить те квантификации, область действия которых не содержит вхождений
квантифицированной переменной. Такие квантификации в действительности не
нужны.
Протаскивание отрицаний. Преобразовать все вхождения отрицания в стоящие
непосредственно перед элементарными подформулами в соответствии со сле-
дующими правилами:
¬∀xA = ∃x¬A;
¬∃xA = ∀x¬A;
¬¬A = A;
¬(A∨B) = ¬A&¬B;
¬(A&B) = ¬A∨¬B.
Перемещение кванторов. С помощью логически эквивалентных преобразова-
ний перемещаем все квантификации в начало формулы. Для этого используется
следующий набор правил преобразования, которые справедливы во всякой тео-
рии первого порядка. Здесь мы приведем эти правила для конъюнкции. Парные
правила для дизъюнкции выглядят аналогично.
(∀x A & ∀x B) = ∀x (A&B).
(∀x A & B) = ∀x (A&B), если B не содержит x.
(A & ∀x B) = ∀x (A&B) , если A не содержит x.
(∃x A & B) = ∃x (A&B) , если B не содержит x.
(A & ∃x B) = ∃x (A&B) , если A не содержит x.
Эти правила позволяют в каждой формуле постепенно передвигать все кванто-
ры влево.
Для полноты этого набора правил необходимо добавить возможность
переименования некоторых связных переменных. Например, формула
∃xA(x) & ∀xB(x) будет сначала преобразована в ∃xA(x) & ∀yB(y) (перед приме-
нением правил преобразования). Заметим также, что для упрощения формул в
34

Страницы