Составители:
Рубрика:
(3.8)
⎤∃vX ↔ ∀v⎤X,
(3.9)
⎤∀vX ↔ ∃v⎤X,
(3.10)
⎤ ⎤X ↔ X,
где X и Y суть формулы, а v – произвольная переменная;
(3.11)
[Y & Z] ∨ X ↔ [Y ∨ X]&[Z ∨ X],
(3.12)
∃vY ∨ X ↔ ∃v[Y ∨ X],
(3.13)
∀vY ∨ X ↔ ∀v[Y ∨ X],
где переменная v не встречается в X;
(3.14)
∀v[X & Y] ↔ ∀vX & ∀vY.
Порядок преобразования формул (предложений) из стандартной
формы в клаузальную следующий.
1. Выполнить стандартизацию переменных, т.е. устранить
случаи, когда одна и та же переменная связана разными
вхождениями одного квантора, например: ∃x[P(x) & ∃xQ(x)].
Применяя правило (3.1), получаем ∃x[P(x) & ∃zQ(z)].
2. Выразить импликацию → и эквивалентность ↔ через ∨, & и
⎤ с помощью правил (3.3-3.5).
3. Переместить отрицания ⎤ внутрь предложений за знаки &, ∨ и
кванторы так, чтобы они оказались непосредственно перед
атомарными формулами. Для этого используются правила (3.6-3.13).
4. Переместить знаки дизъюнкции ∨ внутрь предложений за
знаки & и кванторы так, чтобы знаки ∨ связывали только атомы и
атомы с отрицаниями. Для этого используются правила (3.13).
5. Устранить кванторы существования введением так
называемых функций Сколема (см. ниже) и продвинуть все кванторы
A внутрь конъюнкций с помощью правила (3.14).
6. Перезаписать полученные дизъюнкции атомов и их
отрицаний (иногда называемых дизъюнктами)
A
∨...∨ A ∨⎤B ∨... ⎤B
nm1
B
1
B
в виде клауз
(3.15)
,...,A ← B ,...,B
n
A
.
m1
B
1
B
125
Страницы
- « первая
- ‹ предыдущая
- …
- 39
- 40
- 41
- 42
- 43
- …
- следующая ›
- последняя »
