Математическая логика и теория алгоритмов. Галуев Г.А. - 27 стр.

UptoLike

ВУЗ: 

ТТИ ЮФУ | Таганрог

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

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 27 из 64
© 2003 Галуев Геннадий Анатольевич
GxQxFGxQxF ∨↔∨ )())((
(5.1)
GxQxFGxQxF &)(&))(( ↔
)()( xFxxxF ⎤∃↔⎤∀
(5.2)
)()( xFxxxF ⎤∀↔⎤∃
Здесь
F
формула, содержащая переменную
x
свободно, G - формула, не содер-
жащая переменную
x
.
Законы (5.1), очевидно, истинны, т.к. формула
G не содержит переменную
x
и
поэтому может быть внесена в область действия соответствующего квантора. Приве-
дем еще два закона исчисления предикатов.
)(&)())((&))(( xHxxFxxHxxF ∀
↔
∀∀
(5.3)
)()())(())(( xHxxFxxHxxF ∨∃
↔
∃∨∃
Из законов 5.3 видно, что кванторы
∀
и
∃
можно распределить по & и V соот-
ветственно, т.е. операция навешивания квантора
)( xx
∃
∀
дистрибутивна относительно
операций &(V).
Однако следует знать, что сами кванторы
x
∀
и
)( x
∃
не дистрибутивны относи-
тельно операций V и & , т.е. неверно, что
)()())(())(( xHxxFxxHxxF ∨∀
↔
∀∨∀
(5.4)
)(&)())((&))(( xHxxFxxHxxF ∃
↔
∃∃
В случае, подобном (5.4), следует одну связанную переменную переименовать
в другую, например в Z, после чего воспользоваться законами (5.1).
(
)()())(())(())(())( zHxzFxzzHxxFxxHxxF ∨
∀
∀
↔
∀
∨∀
↔
∀∨∀ (5.5)
(
)(&)())((&))(())((&))( zHxzFxzzHxxFxxHxxF
∃
∃
↔
∃
∃
↔
∃∃ (5.6)
В 5.5, 5.6 предполагается, что формула
)(xF не зависит от переменной Z.
Используя законы (z.1 – z.10), (5.1), (5.2), (5.3), (5.5) и (5.6) любую формулу
исчисления предикатов можно перевести в предваренную нормальную форму. Для
этого формулы приводятся к виду, содержащему только связки &,
¬,V и кванторы;
операции инверсии с помощью законов Де Моргана (z.6) и закона двойного отрица-
ния (z.1) проносят внутрь формулы, после чего кванторы группируются в начале
формулы с помощью законов (5.1)-(5.3), (5.5) и (5.6). Свободные переменные при
этом трактуются как константы.
Приведем пример такого преобразования:
Пусть формула А имеет вид
)()( xxQxxP ∃→⎤∀
из исходной формулы последовательно получаем
⎤
↔∃∀⎤ )())(( xxQVxxP
(по 2.10)
↔∃∀↔ )())(( xxQVxxP (по 2.1.)
↔∃∀↔ ))(())(( xxQVxxP
замена связанной переменной
x
и
.

Страницы