Математическое введение в декларативное программирование. Зюзысов В.М. - 35 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

любой момент можно применять свойства коммутативности, ассоциативности
и идемпотентности связок & и ∨. Итак, теорема конструктивно доказана.
Пример. Найдем предваренную форму, эквивалентную формуле
∀x(P(x) & ∀y∃x(¬Q(x,y) ⊃∀zR(a,x,y))).
Этапы этого поиска последовательно перечислены ниже.
Исключение связки импликации:
∀x(P(x) & ∀y∃x(¬¬Q(x,y) ∨ ∀zR(a,x,y))).
Разделение связных переменных:
∀x(P(x) & ∀y∃u(¬¬Q(u,y) ∨ ∀zR(a,u,y))).
Удаление бесполезной квантификации:
∀x(P(x) & ∀y∃u(¬¬Q(u,y) ∨ R(a,u,y))).
Протаскивание отрицаний:
∀x(P(x) & ∀y∃u(Q(u,y) ∨ R(a,u,y))).
Перемещение кванторов:
∀x∀y (P(x) & ∃u(Q(u,y) ∨ R(a,u,y))),
∀x∀y ∃u (P(x) & (Q(u,y) ∨ R(a,u,y))).
Замечание. Одна формула может допускать много эквивалентных предваренных
форм. Вид полученного результата зависит от порядка применения правил, а также от
произвола при переименовании.
6.3 Сколемизация
Рассмотрим один из математических результатов, послуживших идейной основой
метода резолюций. Интуитивно сочетание кванторов ∀x∃y может пониматься как утвер-
ждение о существовании функции, строящей y по x. Рассмотрим несколько примеров. Ес-
ли замкнутая формула ∃yP(y) выполнима в некоторой интерпретации, то существует неко-
торая предметная константа c из универсума, для которой формула P(с) истинна. Другой
случай. Пусть, например, имеется формула P c двумя параметрами x и y. Тогда замкнутая
формула ∀x∃yP(x,y) выполнима тогда и только тогда, когда выполнима формула
∀xP(x, f(y)), где f – новый одноместный функциональный символ.
Аналогичное преобразование выполнимо и для произвольных предваренных фор-
мул. Например, формула
∀x∀y∃z∀u∃v P(x,y,z,u,v)
выполнима тогда и только тогда, когда выполнима формула
∀x∀y∀u P(x,y, f(x,y),u,g(x,y,u))
(здесь f и g – функциональные символы, не встречающиеся в формуле P).
Элиминация кванторов существования (сколемизация)
Сколемовской формой называется предваренная нормальная форма, не содержащая кван-
торы существования.
Сколемизация осуществляется преобразованиями:
∃x
1
Q
2
x
2
... Q
n
x
n
A(x
1
, x
2
,...,x
n
) → Q
2
x
2
... Q
n
x
n
A(a, x
2
,...,x
n
);
∀x
1
... ∀x
i
-1
∃x
i
Q
i
+1
x
i
+1
... Q
n
x
n
A(x
1
, ..., x
i
,...,x
n
) →
∀x
1
... ∀x
i-
1
Q
i
+1
x
i
+1
... Q
n
x
n
A(x
1
, ..., f( x
1
, ..., x
i
-1
),...,x
n
),
где a − новая предметная константа, f − новый функтор, а Q
2
, ..., Q
n
− любые кванторы,
символ → показывает результат преобразования.
Функции для замены кванторов существования впервые стал использовать
Т. Сколем.
Теорема 8. Пусть даны замкнутая формула A и формула B – результат сколемиза-
ции A. Тогда формулы A и B одновременно выполнимы или невыполнимы.
35

Страницы