ВУЗ:
Составители:
Рубрика:
54
(
∀x)F[x] ∨ (∀x)H[x] ≠ (∀x)(F[x] ∨ H[x]), (12.7)
(
∃x)F[x] ∧ (∃x)H[x]
≠
(∃x)(F[x] ∧ H[x]). (12.8)
В подобных случаях можно поступить следующим образом.
Т.к. каждая связанная переменная в формуле может
рассматриваться лишь как место для подстановки любой
переменной, то каждую связанную переменную x можно
переименовать в z, т.е. (
∀x)H[x] = (∀z)H[z]. Если мы выберем
переменную z, которая не встречается в F[x], то
(
∀x)F[x] ∨ (∀x)H[x] = (∀x)F[x] ∨ (∀z) H[z] =
= (
∀x) (∀z)(F[x] ∨ H[z]) (12.9)
Аналогично
(
∃x)F[x] ∧ (∃x)H[x] = (∃x)F[x] ∧ (∃z) H[z] =
=(
∃x)(∃z)(F[x] H[z]) (12.10)
Т.о., в общем случае имеем
(Q
1
x)F[x] ∨ (Q
2
x)H[x]=(Q
1
x)(Q
2
z)(F[x] ∨ H[z]), (12.11)
(Q
3
x)F[x]
∧
(Q
4
x)H[x]=(Q
3
x)(Q
4
z)(F[x]
∧
H[z]), (12.12)
где Q
1
,Q
2
суть
∀
и ∃, а z не входит в F[x]. Конечно, если Q
1
=Q
2
=∃,
а Q
3
=Q
4
=
∀
, то не обязательно переименовывать переменную x.
Можно напрямую использовать формулы (12.5)-(12.8).
Алгоритм преобразования формул в предваренную нормальную
форму.
Шаг1. Используем
GFGF ∨=→ .
Шаг 2
. Используем
F
F
=
,
или
GFGF
GFGF
∨=∧
∧=∨
или
][)(][)(
],[)(][)(
xFxxFx
xFxxFx
∀=∃
∃=∀
чтобы внести знак отрицания внутрь формулы.
Шаг 3.
Переименовываем связанные переменные, если это
Страницы
- « первая
- ‹ предыдущая
- …
- 52
- 53
- 54
- 55
- 56
- …
- следующая ›
- последняя »