Составители:
Рубрика:
Поясним пункт 5. Для исключения квантора существования ∃
вводится константа или функциональный символ (функция Сколема)
для того, чтобы дать имя значению переменной, на которую неявно
ссылается ∃. Пусть дано множество (конъюнкция) предложений S.
Для исключения ∃ из предложения вида ∀v
∀v ...∀v
n1 2
∃uX, входящего
в S, заменяем это предложение на новое ∀v
∀v ...∀v
n1 2
X', где X'
получено из X заменой всех свободных вхождений u в X на терм
f(v
,...,v
n1
), где f - некоторый функциональный символ, не
встречающийся в S. Если n=0, то терм f(v
,...,v
n1
) сводится к
константному символу.
Отметим, что замена не является эквивалентной и применима
только к высказываниям, но не к формулам со свободными
переменными. Из нового предложения следует исходное, но не
наоборот. Тем не менее, исключение квантора ∃ не оказывает
влияния на совместность результирующего множества клауз.
Приведенные правила (3.1-3.14) являются логической основой
семейства алгоритмов приведения стандартной формы к
клаузальной. Для повышения эффективности алгоритма следует
применять эти правила прежде всего к самым внешним
пропозициональным связкам и заменять формулу с левой стороны
правила эквивалентной формулой с правой стороны.
Число шагов преобразований сокращается, если в процессе
преобразований не заменять импликации →. Для этого полезны
следующие эквивалентности:
(3.16)
[X → Y & Z]↔[X → Y]&[X → Y].
(3.17)
[X ∨ Y → Z]↔[X → Y]&[X → Y].
(3.18)
[X & ⎤Y → Z]↔[X → Y ∨ Z].
(3.19)
[X → ⎤Y ∨ Z]↔[X & Y → Z].
(3.20)
[X →[Y → Z]]↔[X & Y → Z].
(3.21)
[[X → Y]→ Z]↔[X ∨ Y]&[Y → Z].
(3.22)
X → ∀vY ↔ ∀v[X → Y].
(3.23)
X → ∃vY ↔ ∃v[X → Y].
126
Страницы
- « первая
- ‹ предыдущая
- …
- 40
- 41
- 42
- 43
- 44
- …
- следующая ›
- последняя »
