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

UptoLike

ВУЗ: 

СЗТУ | Санкт-Петербург

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

Рубрика: 

множество клауз совместно если и только если совместно исходное
множество предложений в стандартной форме.
Для упрощения в записи формул будем опускать внешние
скобки. Также для упрощения записи в дальнейшем будем считать,
что символы отрицания ⎤ и кванторов ∀ и ∃ задают более тесную
связь, чем другие пропозициональные связки, а символы
конъюнкции & и дизъюнкции ∨ связывают теснее, чем импликация
→ и эквивалентность. С учетом ассоциативности ∨ и & можно,
например, писать
A ∨ B ∨ C ← D & E & F
вместо
[A ∨ [B ∨ C ]] ← [[D & E ] & F].
Кроме того, если из контекста ясно, что формула является
высказыванием, можно опускать квантор всеобщности и, например,
вместо
∀x∀y [планета(y) & вращается_вокруг(x,y) → спутник(x,y)]
писать
планета(y) & вращается_вокруг(x,y) → спутник(x,y).
Для преобразования формул (предложений) из стандартной формы в
клаузальную используется следующая система правил
эквивалентности:
(3.1)
∀uX ↔ ∀v X' и ∃uX ↔ ∃vX',
где X' получается из X заменой всех вхождений u на v, причем v не
встречается в X;
(3.2)
∀vX ↔ X и ∃vX ↔ X,
где переменная v не встречается в X;
(3.3)
[X → Y] ↔ ⎤X ∨ Y,
(3.4)
[X ↔ Y] ↔ [X → Y]&[Y → X], т.е.
(3.5)
[X ↔ Y] ↔ [⎤X ∨ Y]&[ ⎤Y ∨ X];
(3.6)
⎤ [X&Y] ↔ ⎤X ∨ ⎤Y,
(3.7)
⎤ [X∨Y] ↔ ⎤X & ⎤Y,
124

Страницы